2021-03-05 08:24 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001678Frama-CPlug-in > wppublic2014-06-02 16:41
Reporterjens 
Assigned Tocorrenson 
PriorityhighSeveritymajorReproducibilityalways
StatusclosedResolutionduplicate 
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

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

-Notes

~0004929

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.

~0004931

jens (reporter)

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