View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0002312 | Frama-C | Plug-in > wp | public | 2017-06-15 13:39 | 2017-06-15 15:14 | ||||||||
Reporter | Jochen | ||||||||||||
Assigned To | correnson | ||||||||||||
Priority | normal | Severity | tweak | Reproducibility | always | ||||||||
Status | assigned | Resolution | open | ||||||||||
Platform | Phosphorus-20170501-beta1 | OS | xubuntu | OS Version | |||||||||
Product Version | Frama-C 15-Phosphorus | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0002312: false postcondition shouldn't be verified in default memory-model setting | ||||||||||||
Description | Running "frama-c -wp -wp-rte memmodel_default.c" verifies all 11 proof obligations, while the assert clase in line 21 is obviously violated. The reason for Frama-C's behavior is that it assumes the "Hoare Variables mixed with Pointers" memory model as a default (in accordance with WP manual sect.3.4, p.45) without checking its preconditions, viz. the absence of any address-taking of a variable. A novice user who doesn't yet know about the subtleties of memory models will assume after the above Frama-c run that the program is ok, as is has been formally verified. This may build up unjustified trust in the program, and discredit Frama-C (or even the whole field of formal methods) once the bug is detected at runtime, possibly causing severe damage. I suggest to either 1. check the applicability of the "Hoare Variables mixed with Pointers" model (this should be easily achievable, if only the source code needs to be scanned for a unary "&"), or 2. use another, less restrictive, model as default. | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
|
Jochen (reporter) 2017-06-15 15:10 |
Running "frama-c -wp -wp-rte memmodel_default.c -wp-model ref" on the above program verifies all obligations, too. This contradicts the WP manual Sect.3.5 "Hoare Variables for Reference Parameters", p.46, which says "necessary separation conditions are generated on-the-fly". Apparently, no condition "requires \separated(&g,x);" is genarated for foo. If that condition is added manually, it can't be verified (as expected). |