Frama-C Bug Tracking System - Frama-C
View Issue Details
0002390Frama-CPlug-in > wppublic2018-07-24 17:572019-10-17 18:00
closedno change required 
Frama-C 17-Chlorine 
0002390: dubious discharge of postcondition
Consider the following function /*@ assigns \nothing; ensures a == 0; */ void foo(int a) { a = 0; } The postcondition can of course not be verified because the assignment happens to a copy "a" and furthermore nothing is known about the value of "a" in the pre-state. If I add, however, the admittedly weird looking precondition "requires \valid(&a);" as shown here /*@ requires \valid(&a); assigns \nothing; ensures a == 0; */ void bar(int a) { a = 0; } then Qed discharges the postcondition. I am not sure this a bug or rather caused by taking the address of a formal argument in the precondition but in any case it would be nice if someone could have a look at it.
Call frama-c -wp -wp-rte foo.c on the attached file.
No tags attached.
c foo.c (187) 2018-07-24 17:57
Issue History
2018-07-24 17:57jensNew Issue
2018-07-24 17:57jensStatusnew => assigned
2018-07-24 17:57jensAssigned To => correnson
2018-07-24 17:57jensFile Added: foo.c
2018-07-25 14:20corrensonNote Added: 0006607
2018-07-25 14:20corrensonNote Added: 0006608
2018-07-25 14:20corrensonStatusassigned => resolved
2018-07-25 14:20corrensonResolutionopen => no change required
2018-07-25 14:22corrensonNote Added: 0006609
2018-07-25 14:33virgileNote Added: 0006610
2018-07-25 14:44jensNote Added: 0006611
2018-07-25 14:44jensStatusresolved => feedback
2018-07-25 14:44jensResolutionno change required => reopened
2018-07-25 14:48virgileNote Added: 0006612
2018-07-25 15:06corrensonNote Added: 0006614
2018-07-25 15:25virgileNote Added: 0006615
2019-10-17 17:07corrensonStatusfeedback => resolved
2019-10-17 17:07corrensonResolutionreopened => no change required
2019-10-17 18:00signolesStatusresolved => closed

2018-07-25 14:20   
Indeed, formals are not (yet) allocated in the pre-state, although they are allocated just before the first statement of the body... This is a corner case, of course. Typically, the following program is proven: *@ requires \valid(&a); ensures \false; */ void f(int a) { return ; } But, then, the following one fails with a WP error: void g(int x) { f(x); } [wp] User Error: Address of logic value (x_0) This is because, when you instantiate the pre-condition of f with the formal parameters, you get an incorrect expression with (&a).
2018-07-25 14:20   
Formals not allocated in the pre-state
2018-07-25 14:22   
Side note : we are also working on running smoke tests to detect infeasible requires (those that would allow to prove false). Second side node : probably it would be a good idea to detect the usage of (&x) on a formal (x) inside pre-conditions.
2018-07-25 14:33   
Third side note: this would also warrant a clarification in the ACSL manual itself, because at the moment there is nothing in it that precludes the usage of \valid(&a) in a requires. By the way what would be the status of \valid(&a) in an ensures clause?
2018-07-25 14:44   
Shall I create a request for clarification in the ACSL manual?
2018-07-25 14:48   
@jens, That'd be great, thanks
2018-07-25 15:06   
For the same reason, `\valid(&a)` is not valid in the ensures clause, also it is still valid just at the end of the body. Although, `\valid(&a)` reveals the same problem of accessing the address of values when used at call-sites. Actually, the Kernel shall reject any access to the address of a formal inside a function specification.
2018-07-25 15:25   
this will be on the todo list as soon as this point of view is endorsed by the ACSL manual 😛