GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity

Add regression tests for the ignore-safety option

Browse Source
This commit is contained in:
Rob Dockins 2020-07-14 12:09:05 -07:00
parent bc0545bd62
commit c2c1ad1231
2 changed files with 41 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
tests/regression/ignore-safe.icry Normal file
View File

@ -0,0 +1,26 @@
:set prover-stats = off
:set show-examples = off
:set ignore-safety = off
:prove (\ (x:Integer) -> 0 < x ==> x < 4 ==> [3,2,1]@x == 3-x)
:prove (\ (x:[8]) -> x < 4 ==> [3,2,1]@x == 3-x)
:prove (\ (x:Integer) y -> (y == 0) || (y*(x/y) + x%y == x))
:prove (\ (x:[8]) y -> (y == 0) || (y*(x/y) + x%y == x))
:prove (\ (x:Integer) -> [0,0,0]@x == 0 )
:prove (\ (x:Integer) -> []@x == 0 )
:prove (\ (x:[8]) -> [0,0,0]@x == 0 )
:set ignore-safety = on
:prove (\ (x:Integer) -> 0 < x ==> x < 4 ==> [3,2,1]@x == 3-x)
:prove (\ (x:[8]) -> x < 4 ==> [3,2,1]@x == 3-x)
:prove (\ (x:Integer) y -> (y == 0) || (y*(x/y) + x%y == x))
:prove (\ (x:[8]) y -> (y == 0) || (y*(x/y) + x%y == x))
:prove (\ (x:Integer) -> [0,0,0]@x == 0 )
:prove (\ (x:Integer) -> []@x == 0 )
:prove (\ (x:[8]) -> [0,0,0]@x == 0 )

15
tests/regression/ignore-safe.icry.stdout Normal file
View File

@ -0,0 +1,15 @@
Loading module Cryptol
Counterexample
Counterexample
Counterexample
Counterexample
Counterexample
Counterexample
Counterexample
Q.E.D.
Q.E.D.
Q.E.D.
Q.E.D.
Q.E.D.
Q.E.D.
Q.E.D.