| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001678 | Frama-C | Plug-in > wp | public | 2014-03-07 13:27 | 2014-06-02 16:41 | ||||
| Reporter | jens | ||||||||
| Assigned To | correnson | ||||||||
| Priority | high | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | duplicate | ||||||
| Platform | OS | Linux, OSX | OS Version | ||||||
| Product Version | Frama-C Fluorine-20130601 | ||||||||
| Target Version | Fixed in Version | ||||||||
| Summary | 0001678: Frama-C/WP does not warn about unsatisfied precondition | ||||||||
| Description | Here is the setup: /*@ requires 0 < a ; assigns \nothing; ensures 0 < \result < 10; */ int foo(int a); /*@ assigns \nothing; ensures 0 < \result < 30; */ int bar(int x) { int a = foo(1); // precondition satisfied int b = foo(0); // precondition violated and recognized int c = foo(x); // precondition not satisfied and not recognized return a + b + c; } When I process this example with frama-c-gui -wp -cpp-command 'gcc -C -E -I.' -pp-annot -wp-rte -no-unicode -wp-out ./out.wp -wp-proof alt-ergo -wp-proof coq foo.c then a green bullet appears next to the line int c = foo(x); // precondition not satisfied and not recognized However, it is unknown whether x satisfies the precondition "0 < x" of foo. If, however, the lines are reverse like this int c = foo(x); int b = foo(0); then both calls are correctly flagged as orange (yellow?) | ||||||||
| Additional Information | The problem also appears in the release candidate for Neon. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
||||||
|
||||||
 Relationships |
| Notes |
|
|
correnson (manager) 2014-03-07 14:09 Last edited: 2014-03-07 14:11 |
This an instance of assert false in the context. Actually, the pre-condition at second call to foo() normalizes to false (0<0 ==> false). Formally, this is not a bug, but I agree on the fact that this is confusing for the user. For instance, try this: # frama-c-gui -main bar -val -wp bar.c Value would show you the dead code! We have already an issue on detecting such inconsistencies and trying to avoid using 'false' assertions as hypotheses in other goals. |
|
jens (reporter) 2014-03-08 20:05 |
Hello Loïc, thank you for the explanation and sorry for reporting something as "major" that isn't really a bug. Jens |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2014-03-07 13:27 | jens | New Issue | |
| 2014-03-07 13:27 | jens | Status | new => assigned |
| 2014-03-07 13:27 | jens | Assigned To | => correnson |
| 2014-03-07 14:09 | correnson | Note Added: 0004929 | |
| 2014-03-07 14:11 | correnson | Note Edited: 0004929 | View Revisions |
| 2014-03-08 20:05 | jens | Note Added: 0004931 | |
| 2014-06-02 16:40 | correnson | Relationship added | related to 0001537 |
| 2014-06-02 16:41 | correnson | Status | assigned => closed |
| 2014-06-02 16:41 | correnson | Resolution | open => duplicate |
| Issue History |