2021-03-05 08:24 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001678Frama-CPlug-in > wppublic2014-06-02 16:41
Assigned Tocorrenson 
PlatformOSLinux, OSXOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in Version 
Summary0001678: Frama-C/WP does not warn about unsatisfied precondition
DescriptionHere 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 InformationThe problem also appears in the release candidate for Neon.
TagsNo tags attached.
Attached Files

related to 0001537acknowledgedcorrenson Frama-C should warn about inconsistent specification of declared functions 



correnson (manager)

Last edited: 2014-03-07 14:11

View 2 revisions

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)

Hello Loïc,

thank you for the explanation and sorry for reporting something as "major" that isn't really a bug.


-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