-
Notifications
You must be signed in to change notification settings - Fork 8
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
Taking the address of a formal in a function contract #49
Comments
Loïc's said under https://bts.frama-c.com/view.php?id=2390 that
This seems strange to me, as the pre-state can (of course) refer to the value of formals. And, if we accept that they are in scope in the pre-state, I don't see why we would reject terms that take their address. This is probably not very useful, but not worth rejecting either. In the post-state, Frama-C's kernel has already taken a stance, since we add |
@yakobowski I tend to agree with the fact that this is a bit strange, but at the same time, the fact that formals retain their original value in the |
I also think it is strange to say the formals are not (yet) allocated in the pre-state because we talk about their values in the preconditions. I tend to reject taking the address of a formal argument in the contract. Is there a meaningful usage of such an address for the caller ? On the other hand, it might be "necessary" in a contract to take the address
Should one disallow/discourage such predicates? |
The caller does not have access to the addresses of the formals indeed, but your example of a predicate taking a pointer as argument is interesting (even though I'd expect to see pretty few examples of that in real applications). |
Well, we tend to create predicates taking pointers as arguments since we cannot reason on sets of locations without this mechanism. Regarding e.g. addresses of formals in the post-state, I was going to suggest banishing them when not under a |
Virgile mentioned references. Maybe one could used references in ACSL predicates... |
Of course, it could be useful to take the address of formals, but as far I remember, specifications taking such an address can be always rewritten without taking that address. Here there is two example where in C the address of formals has to be taken, but this is not necessary in the ACSL specifications:
|
(backported from Frama-C's bts)
In 0002390 the issue was raised whether functions contracts such as
are meaningful.
More specifically, the ACSL manual should clarify whether using the address of a formal argument in a precondition, and more generally a function contract, is illegal.
The text was updated successfully, but these errors were encountered: