|Anonymous | Login | Signup for a new account||2017-12-15 20:33 CET|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|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|
|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||memmodel_default.c [^] (273 bytes) 2017-06-15 13:39 [Show Content]|
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).
|2017-06-15 13:39||Jochen||New Issue|
|2017-06-15 13:39||Jochen||Status||new => assigned|
|2017-06-15 13:39||Jochen||Assigned To||=> correnson|
|2017-06-15 13:39||Jochen||File Added: memmodel_default.c|
|2017-06-15 15:10||Jochen||Note Added: 0006410|
|Copyright © 2000 - 2017 MantisBT Team|