| View Issue Details [ Jump to Notes ] | [ 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 | ||||||
| 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 |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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. |
|
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... |
|
yakobowski (manager) 2014-02-12 16:58 |
Fix committed to stable/neon branch. |
| Notes |
| Issue History |
|||
| 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 | ||
| 2013-05-30 14:23 | svn | Status | assigned => resolved |
| 2013-05-30 14:23 | svn | Resolution | open => fixed |
| 2013-12-19 01:11 | yakobowski | Source_changeset_attached | => framac master 6bf807f4 |
| 2014-02-12 16:53 | yakobowski | Source_changeset_attached | => framac stable/neon 6bf807f4 |
| 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 |
| Issue History |