Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001435Frama-CPlug-in > Evapublic2013-05-30 10:202014-03-13 15:57
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130501 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001435: The post-conditon of [gets] got status invalid
DescriptionWhen 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 InformationExample :

$ 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);
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(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.

- 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 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
Powered by Mantis Bugtracker