false postcondition shouldn't be verified in default memory-model setting
ID0002312: This issue was created automatically from Mantis Issue 2312. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002312 | Frama-C | Plug-in > wp | public | 2017-06-15 | 2017-06-15 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | tweak | Reproducibility | always |
| Platform | Phosphorus-20170501-beta1 | OS | xubuntu | OS Version | - |
| Product Version | Frama-C 15-Phosphorus | Target Version | - | Fixed in Version | - |
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
- 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
- use another, less restrictive, model as default.