View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000381 | Frama-C | Plug-in > Eva | public | 2010-01-21 17:19 | 2014-02-12 16:56 | ||||
Reporter | lalande | ||||||||
Assigned To | pascal | ||||||||
Priority | normal | Severity | feature | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Beryllium-20090901 | ||||||||
Target Version | Fixed in Version | Frama-C Boron-20100401 | |||||||
Summary | 0000381: propagation of \result clauses | ||||||||
Description | Hello, when discovering Frama-C, I tried to specify some clauses on some functions to specify constraints on the return statement. But it seems that the "ensures" clauses that are "unknown" are not propagated after the analysis of the function. For example: /*@ensures \result >= 0; @ensures \result <= 10; int fonc() { int y = rand(); return y; } int main() { u = fonc(); } gives y in [--;--] u in [--;--] The @assert seems to be propagated, whereas the constraints on \result not. I got a response of one of the developer that says that this is in the TODO list... Is it right ? Best regards, JF Lalande. | ||||||||
Additional Information | Frama-C Beryllium 2009-09-01 | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
signoles (manager) 2010-01-21 17:36 |
See also the today thread on Frama-C discuss : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-January/001759.html. |
pascal (reporter) 2010-02-23 22:49 Last edited: 2010-02-23 22:50 |
Fixing miscellaneous syntax errors in the example, the development versin now produces: [value] Values for function main: u IN [0..10] Note that you can also write 0 <= u <= 10 ; for the post-condition, it is a tad more concise. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2010-01-21 17:19 | lalande | New Issue | |
2010-01-21 17:36 | signoles | Note Added: 0000648 | |
2010-01-21 17:36 | signoles | Assigned To | => pascal |
2010-01-21 17:36 | signoles | Status | new => assigned |
2010-01-21 17:36 | signoles | Category | kernel => plug-in > value analysis |
2010-01-21 17:36 | signoles | Additional Information Updated | |
2010-02-23 22:49 | pascal | Note Added: 0000712 | |
2010-02-23 22:50 | pascal | Note Edited: 0000712 | |
2010-02-23 22:51 | pascal | Status | assigned => resolved |
2010-02-23 22:51 | pascal | Fixed in Version | => Frama-C Bore |
2010-02-23 22:51 | pascal | Resolution | open => fixed |
2010-04-13 15:30 | signoles | Status | resolved => new |
2010-04-13 15:31 | signoles | Status | new => closed |
2013-12-19 01:14 | signoles | Source_changeset_attached | => framac master 00128456 |
2014-02-12 16:56 | signoles | Source_changeset_attached | => framac stable/neon 00128456 |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |