Anonymous | Login | Signup for a new account | 2019-02-17 03:57 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
0001369 | Frama-C | Plug-in > Eva | public | 2013-02-15 11:59 | 2014-03-13 15:57 | ||||
Reporter | Jochen | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | OS | OS Version | |||||||
Product Version | Frama-C Oxygen-20120901 | ||||||||
Target Version | Frama-C Neon-20140301 | Fixed in Version | Frama-C Neon-20140301 | ||||||
Summary | 0001369: strange warning "postcondition got status invalid" | ||||||||
Description | Running "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. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files | ![]() | ||||||||
![]() |
|
(0003696) yakobowski (manager) 2013-02-15 13:06 |
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 http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2012-April/003182.html [^] http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2012-November/003445.html [^] |
(0003959) Jochen (reporter) 2013-06-13 15:52 |
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? |
(0004861) yakobowski (manager) 2014-02-25 14:43 |
Fix committed to feature/neon-doc-value branch. |
(0004862) yakobowski (manager) 2014-02-26 19:57 |
Fix committed to stable/neon branch. |
![]() |
|||
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 | 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 | 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 |
Copyright © 2000 - 2019 MantisBT Team |