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.