2021-02-27 04:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001369Frama-CPlug-in > Evapublic2014-03-13 15:57
Assigned Toyakobowski 
Product VersionFrama-C Oxygen-20120901 
Target VersionFrama-C Neon-20140301Fixed in VersionFrama-C Neon-20140301 
Summary0001369: strange warning "postcondition got status invalid"
DescriptionRunning "frama-c -val ftest.c" on the attached program produces a "[value] Function foo: postcondition got status invalid" in line 6, although the ensures clause looks quite reasonable. (I don't understand the notion of a "postcondition status": shouldn't the postconditions of a function be satisfied automatically if all its preconditions are?) The warning disappears if the ensures clause in line 5 is removed or an appropriate function body (e.g. the one commented out at the end of line 6) is added.
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (140 bytes) 2013-02-15 11:59 -
    static char *p;
    /*@ assigns \nothing;
        ensures \result == p; */
    char *foo(void); //{ return p; }
    void main(void) { foo(); }
    c file icon ftest.c (140 bytes) 2013-02-15 11:59 +




yakobowski (manager)

Hello Jochen.

Value evaluates functions without a body by looking at their assigns clauses. However, in order (1) to remain sound (2) to keep some precision, it makes a restrictive interpretation of what can be written in the assigned zones. Unlike what happens for WP, you cannot just write "assigns foo, bar; ensures bar = baz". Instead, you must write something like "assigns foo \from \nothing, bar \from baz; ensures bar = baz". In short, you _must_ write 'from' clauses, except in very simple cases.

I'm going to refer you to two discussions in the Frama-C list. The first one discusses your exact problem, ie. a function that returns a global pointer (for which you currently need a hack). Do they make things clearer for you? I'm also in the process of improving the relevant section of the manual for Fluorine



Jochen (reporter)

Hello Boris,

from the April blog article (003182.html), I understand that I should always provide \from in an assigns clause; when I do that on the ftest.c program, the message changes from "... got status invalid" to "... got status unknown", which sounds better.

I don't know the interiors of Value good enough to understand your blog explanations involving "post-assigns state" and "alloced_return_..." etc; they seem to explain a difference between pointer- and non-pointer-types. Maybe, an end-user need not understand these details.

In any case, it would be useful if the hint "add a \from part to your assigns" (or even "add an assigns clause at all, and equip it with a \from part") would be given by the FRAMA-C output. In the manual, some simple/naive explanation about the meaning of the message "postcondition got status invalid" and "... unknown" would be helpful.

Did I understand you right: Value tries to validate an ensures clause even if no code is given for an external function; the only clues it has in that case are the assigns clauses, which better had a \from part. The message "...unknown" means "you user are responsible yourself for validating that function contract, if you don't show me the body code"; while "...invalid" means "although I couldn't check with the body code, the ensures clause must be wrong, as it contradicts (somehow) the assigns clause". Or am I wrong with that?


yakobowski (manager)

Fix committed to feature/neon-doc-value branch.


yakobowski (manager)

Fix committed to stable/neon branch.

-Issue History
Date Modified Username Field Change
2013-02-15 11:59 Jochen New Issue
2013-02-15 11:59 Jochen Status new => assigned
2013-02-15 11:59 Jochen Assigned To => yakobowski
2013-02-15 11:59 Jochen File Added: ftest.c
2013-02-15 13:06 yakobowski Note Added: 0003696
2013-02-15 13:06 yakobowski Status assigned => feedback
2013-05-30 23:21 yakobowski Target Version => Frama-C Neon-20140301
2013-06-13 15:52 Jochen Note Added: 0003959
2014-02-25 14:43 yakobowski Source_changeset_attached => framac feature/neon-doc-value 19051169
2014-02-25 14:43 yakobowski Note Added: 0004861
2014-02-25 14:43 yakobowski Resolution open => fixed
2014-02-25 17:40 signoles Status feedback => resolved
2014-02-26 19:57 yakobowski Source_changeset_attached => framac stable/neon 19051169
2014-02-26 19:57 yakobowski Note Added: 0004862
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History