-
Notifications
You must be signed in to change notification settings - Fork 250
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
CBMC 5.95.1 crashes on proof of simple array equality function #8298
Comments
In loop contracts, we replace quantified variables with a tmp variable and add the tmp variable to the symbol map. However, the detection of the quantified variables is not complete now: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/utils.cpp#L425. It does not include equal expression. The error doesn't persist once I add the equal expression to the detection. |
As a workaround before the fix is merged, you may want to use the boolean variable |
Please let me know when this fix is merged. |
I tried inverting the logic and using != instead of ==, but I don't like it because it makes the code much harder to read and understand. With that change, I get 2 warnings that say "warning: ignoring forall" which are followed by a print out of some syntax tree. What does that mean? |
The SAT backend eagerly grounds quantifiers when domains are small, but ignores them when domains are too large, which is seems to be the case here. You should try using the SMT back-end to solve this example, quantifiers are passed to the SMT back-end and grounded using the solver's heuristics. |
OK. Please improve the error message to make it clearer what's wrong and what the corrective action should be. |
#8299 was merged. |
CBMC version: 5.95.1
Operating system: macOS 13.6.6
Exact command line resulting in the issue: See linked GitHub Repo
What behaviour did you expect: proof
What happened instead: crash.
CBMC crashes trying to prove correctness of a simple function that compares arrays for equality.
See code in
https://github.com/rod-chapman/cbmc-examples/blob/20a559b99287945ab8a390689b14fb35316ea882/arrays/ar.c#L169
In that directory, the command
make TARGET=constant_time_equals_strict
produces
The text was updated successfully, but these errors were encountered: