Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add option to specify when we expect a counterexample #177

Open
karmacoma-eth opened this issue Aug 15, 2023 · 0 comments
Open

Add option to specify when we expect a counterexample #177

karmacoma-eth opened this issue Aug 15, 2023 · 0 comments
Labels
enhancement New feature or request good first issue Good for newcomers

Comments

@karmacoma-eth
Copy link
Collaborator

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

@karmacoma-eth karmacoma-eth added enhancement New feature or request good first issue Good for newcomers labels Aug 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request good first issue Good for newcomers
Projects
None yet
Development

No branches or pull requests

1 participant