Anonymous | Login | Signup for a new account | 2019-12-08 06:28 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
0002390 | Frama-C | Plug-in > wp | public | 2018-07-24 17:57 | 2019-10-17 18:00 | ||||
Reporter | jens | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | no change required | ||||||
Platform | OS | OS Version | |||||||
Product Version | Frama-C 17-Chlorine | ||||||||
Target Version | Fixed in Version | ||||||||
Summary | 0002390: dubious discharge of postcondition | ||||||||
Description | 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. | ||||||||
Steps To Reproduce | Call frama-c -wp -wp-rte foo.c on the attached file. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files | ![]() | ||||||||
![]() |
|
(0006607) correnson (manager) 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). |
(0006608) correnson (manager) 2018-07-25 14:20 |
Formals not allocated in the pre-state |
(0006609) correnson (manager) 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. |
(0006610) virgile (developer) 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? |
(0006611) jens (reporter) 2018-07-25 14:44 |
Shall I create a request for clarification in the ACSL manual? |
(0006612) virgile (developer) 2018-07-25 14:48 |
@jens, That'd be great, thanks |
(0006614) correnson (manager) 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. |
(0006615) virgile (developer) 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 😛 |
![]() |
|||
Date Modified | Username | Field | Change |
2018-07-24 17:57 | jens | New Issue | |
2018-07-24 17:57 | jens | Status | new => assigned |
2018-07-24 17:57 | jens | Assigned To | => correnson |
2018-07-24 17:57 | jens | File Added: foo.c | |
2018-07-25 14:20 | correnson | Note Added: 0006607 | |
2018-07-25 14:20 | correnson | Note Added: 0006608 | |
2018-07-25 14:20 | correnson | Status | assigned => resolved |
2018-07-25 14:20 | correnson | Resolution | open => no change required |
2018-07-25 14:22 | correnson | Note Added: 0006609 | |
2018-07-25 14:33 | virgile | Note Added: 0006610 | |
2018-07-25 14:44 | jens | Note Added: 0006611 | |
2018-07-25 14:44 | jens | Status | resolved => feedback |
2018-07-25 14:44 | jens | Resolution | no change required => reopened |
2018-07-25 14:48 | virgile | Note Added: 0006612 | |
2018-07-25 15:06 | correnson | Note Added: 0006614 | |
2018-07-25 15:25 | virgile | Note Added: 0006615 | |
2019-10-17 17:07 | correnson | Status | feedback => resolved |
2019-10-17 17:07 | correnson | Resolution | reopened => no change required |
2019-10-17 18:00 | signoles | Status | resolved => closed |
Copyright © 2000 - 2019 MantisBT Team |