The post-conditon of [gets] got status invalid
ID0001435: This issue was created automatically from Mantis Issue 1435. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001435 | Frama-C | Plug-in > Eva | public | 2013-05-30 | 2014-03-13 |
| Reporter | Anne | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130501 | Target Version | - | Fixed in Version | Frama-C Neon-20140301 |
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="-Iframa-c -print-path/libc -nostdinc"
#include <stdio.h> void main () { char line[100]; char * p = gets (line); }