GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 21:11:35 +03:00
Code Issues Projects Releases Wiki Activity
13363c4c9b
cryptol/tests/issues/issue093.icry.stdout

31 lines
613 B
Plaintext
Raw Normal View History

implicit :prove all properties when no argument given closes #93
2014-09-09 23:27:46 +04:00
Loading module Cryptol
Loading module Cryptol
Loading module Main
property t0 Using exhaustive testing.
refactor :check and :exhaust This is to set up improvements to the cryptol-server, and therefore pycryptol interface. This patch also fixes a regression in pretty-printing output caused by a previous error in fixity of the `<>` operator
2015-12-23 05:17:20 +03:00
testing...passed 1 tests.
wrt #132 update the expected output for the tests.
2014-10-24 01:27:06 +04:00
Q.E.D.
implicit :prove all properties when no argument given closes #93
2014-09-09 23:27:46 +04:00
property t1 Using random testing.
fix #93 Revised how we do output for `:sat` and `:prove` without arguments, making it more clear what properties are being checked in each case. Also reworded the output of `:check` slightly in the case where the property has no inputs. It would be nice to make `:check` output more consistent with the others.
2015-02-18 21:25:46 +03:00
testing...passed 100 tests.
Change how test coverage statistics are computed. This formulation accounts for the fact that test vectors are chosen randomly with replacement. Fixes #461
2017-10-04 03:36:41 +03:00
Expected test coverage: 0.00% (100 of 2^^32 values)
implicit :prove all properties when no argument given closes #93
2014-09-09 23:27:46 +04:00
property t2 Using random testing.
fix #93 Revised how we do output for `:sat` and `:prove` without arguments, making it more clear what properties are being checked in each case. Also reworded the output of `:check` slightly in the case where the property has no inputs. It would be nice to make `:check` output more consistent with the others.
2015-02-18 21:25:46 +03:00
testing...passed 100 tests.
Change how test coverage statistics are computed. This formulation accounts for the fact that test vectors are chosen randomly with replacement. Fixes #461
2017-10-04 03:36:41 +03:00
Expected test coverage: 0.00% (100 of 2^^64 values)
Fix test output for issue093. Since #171 was fixed in b77dd2a8, the tests and proofs are run in the order they appear in the source file.
2016-05-31 20:34:51 +03:00
property f0 Using exhaustive testing.
Fix test output due to counterexample printing change.
2017-09-30 00:23:18 +03:00
testing...f0 = False
fix #93 Revised how we do output for `:sat` and `:prove` without arguments, making it more clear what properties are being checked in each case. Also reworded the output of `:check` slightly in the case where the property has no inputs. It would be nice to make `:check` output more consistent with the others.
2015-02-18 21:25:46 +03:00
:prove t0
Q.E.D.
:prove t1
Q.E.D.
:prove t2
Q.E.D.
Fix test output for issue093. Since #171 was fixed in b77dd2a8, the tests and proofs are run in the order they appear in the source file.
2016-05-31 20:34:51 +03:00
:prove f0
f0 = False
fix #93 Revised how we do output for `:sat` and `:prove` without arguments, making it more clear what properties are being checked in each case. Also reworded the output of `:check` slightly in the case where the property has no inputs. It would be nice to make `:check` output more consistent with the others.
2015-02-18 21:25:46 +03:00
:sat t0
t0 = True
:sat t1
t1 0x00000000 = True
:sat t2
switch to Z3 for typechecking and proving Note: the hardcoding in this patch is only for the 2.2 hotfix branch; in the 2.3 branch we will only have to change the default setting for the typechecker.
2015-12-24 01:59:10 +03:00
t2 0xfffffffe 0xffffffff = True
Fix test output for issue093. Since #171 was fixed in b77dd2a8, the tests and proofs are run in the order they appear in the source file.
2016-05-31 20:34:51 +03:00
:sat f0
Unsatisfiable
Reference in New Issue Copy Permalink