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="-I`frama-c -print-path`/libc -nostdinc" #include <stdio.h> void main () { char line[100]; char * p = gets (line); }