0001435: The post-conditon of [gets] got status invalid - Frama-C Bug Tracking System

Frama-C Bug Tracking System

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 void main () { char line[100]; char * p = gets (line); }

Tags

No tags attached.

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 - 2020 MantisBT Team