halmos
halmos copied to clipboard
Add option to specify when we expect a counterexample
Currently:
- tests with no counterexamples return 0 and a green
[PASS]
- tests with counterexamples, or
unknown
results return non-0 and a red[FAIL]
This makes running the test suite a little scary, because we see a mix of [PASS]
and [FAIL]
but sometimes [PASS]
can be bad (if we expected a counterexample) and [FAIL]
can be bad (if we didn't expect a counterexample).
We should add the --expect-counterexample
option (open to better naming suggestions):
- tests that do have 1 or more counterexamples return exitcode 0 and a green
[XFAIL]
(for "expected fail" -- we found the thing we're looking for) - tests that fail with no counterexamples are still a red
[FAIL]
(it fails for unexpected reasons), they return exitcode != 0 - tests that would normally be a green
[PASS]
are now a red[XPASS]
(for "unexpected pass" -- we didn't find the thing we're looking for), they return exitcode != 0
Similarly, we should have an --expect-fail
option that behaves similarly but for tests that fail with no counterexamples.
Then we can add the right /// @custom:halmos --expect-counterexample
annotations to solidity tests and running halmos --root tests
should output a mix of green [PASS]
and [XFAIL]
and return 0