-
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
Discrepancy between API specification and behavior for __CPROVER_r_ok #8199
Comments
With regard to documentation, are you referring to the following: "If p is neither null nor valid, the semantics is unspecified." This doesn't say anything to the effect of "undefined behavior" (which is a term very specific to the C language/the C standard). If there is any place where we claim "undefined behavior," then we need to fix that documentation. |
Fair, I don't think UB shows up in the documentation. However, writing proofs that rely on unspecified semantics is still wrong and potentially unsound. |
How about: "If p is neither null nor valid, it is unspecified whether the predicate evaluates to true or false." |
Unspecified semantics means that it is ok to always be true, which will make proofs unsound. @remi-delmas-3000 @zhassan-aws any suggestions on how to capture the expected behavior? |
Let me first make sure that we agree on what it means to be sound here. My take on that is that an analysis (in this case: bounded model checking of the given C program) is sound for a given property p, if, and only if, it reports that p holds on that given program when p holds for all possible executions of the program under the semantics specified by the C language standard (pick your version) plus any additional specification of semantics given in our documentation when we the program uses language extensions provided by CBMC. For the given example program, it seems sufficient to consider three equivalence classes of possible executions:
So: in what way does this make proofs unsound? |
The execution 3 is the one that I was considering unsound, but I agree with you that according to the API specification this is perfectly fine. It sounds that this is a misunderstanding on my part that using this API inside an assertion should be safe even if the pointer is invalid. But this is not correct, and it only applies today given its current implementation. |
@tautschnig Indeed if we agree that However this also implies that I have looked at how |
I totally agree @remi-delmas-3000. I created #8217 to capture the request to provide an API to detect invalid pointers. |
Reopening this based on this comment: #8217 (comment) |
CBMC version: 5.95.1
Operating system: Ubuntu 22.04
Exact command line resulting in the issue:
cbmc main.c
What behaviour did you expect: I expected the specification to say that the
__CPROVER_r_ok
returns non-deterministic value for non-null invalid pointers.What happened instead: The specification explicitly says that calling
__CPROVER_r_ok
with invalid pointer has undefined behavior. Hence, I can only conclude that theassert(__CPROVER_r_ok())
will fail if the pointer is null.I.e.: According to the specification, the following implementation would be perfectly fine:
Which would make the following snippet unsound unless if user invokes it with
--pointer-primitive-check
:The text was updated successfully, but these errors were encountered: