Frama-C/WP does not warn about unsatisfied precondition
ID0001678: This issue was created automatically from Mantis Issue 1678. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001678 | Frama-C | Plug-in > wp | public | 2014-03-07 | 2014-06-02 |
| Reporter | jens | Assigned To | correnson | Resolution | duplicate |
| Priority | high | Severity | major | Reproducibility | always |
| Platform | - | OS | Linux, OSX | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | - |
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.