Anonymous | Login | Signup for a new account | 2019-02-21 12:03 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 | ||||
0001435 | Frama-C | Plug-in > Eva | public | 2013-05-30 10:20 | 2014-03-13 15:57 | ||||
Reporter | Anne | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | OS | OS Version | |||||||
Product Version | Frama-C Fluorine-20130501 | ||||||||
Target Version | Fixed in Version | Frama-C Neon-20140301 | |||||||
Summary | 0001435: The post-conditon of [gets] got status invalid | ||||||||
Description | When using 'gets' from Frama-C include files, the value analysis gives : :/usr/local/share/frama-c/libc/stdio.h:225: [value] Function gets: postcondition got status invalid. I don't really understand how Value can say something about the post-condition of an undefined function, but anyway, then I get "This call never terminates". It seems that a fix is to add : @ assigns \result \from s, *__fc_stdin; but maybe it could be more correct to also add : @ assigns *__fc_stdin \from *__fc_stdin ; | ||||||||
Additional Information | Example : $ frama-c -val toto.c -cpp-extra-args="-I`frama-c -print-path`/libc -nostdinc" #include <stdio.h> void main () { char line[100]; char * p = gets (line); } | ||||||||
Tags | No tags attached. | ||||||||
Attached Files | |||||||||
![]() |
|
(0003921) yakobowski (manager) 2013-05-30 11:40 |
Your fix is correct, thanks. Evaluation of post-condition is needed to reduce the state coming from the assigns. However, we probably should write a different big scary message when the post-condition of those functions get status invalid, at it usually indicates a wrong post-condition instead of a real status. |
(0003922) Anne (reporter) 2013-05-30 12:03 |
Yes : it is quite dangerous if one doesn't notice it since it can lead to too much dead code, and dead code is not so easy to analyze on a large application... |
(0004574) yakobowski (manager) 2014-02-12 16:58 |
Fix committed to stable/neon branch. |
![]() |
|||
Date Modified | Username | Field | Change |
2013-05-30 10:20 | Anne | New Issue | |
2013-05-30 10:20 | Anne | Status | new => assigned |
2013-05-30 10:20 | Anne | Assigned To | => yakobowski |
2013-05-30 11:40 | yakobowski | Note Added: 0003921 | |
2013-05-30 12:03 | Anne | Note Added: 0003922 | |
2013-05-30 14:23 | svn | Checkin | |
2013-05-30 14:23 | svn | Status | assigned => resolved |
2013-05-30 14:23 | svn | Resolution | open => fixed |
2014-02-12 16:58 | yakobowski | Note Added: 0004574 | |
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 |