Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000289Frama-CPlug-in > jessiepublic2009-10-19 14:372010-06-09 18:09
ReporterSylvain Boulme 
Assigned Tovirgile 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in Version 
Summary0000289: unsoundness of Jessie with respect to expression evaluation of ANSI-C
DescriptionThe following program is completely proved by Jessie (using Alt-Ergo 0.9). However, when compiled with gcc on my Linux-PC, it leads to a segmentation fault. The problem seems to come from the fact that Jessie chooses an order of evaluation for subexpressions which is different from my gcc. Actually ANSI-C specifies that the order of evaluation is indeterminate. Some hints to fix this problem: + detect and forbids expressions which depend on evaluation order. + alternatively, emulate the semantics of x = c - decr() by if (anybool()) { tmp_l=c ; tmp_r=decr() ; } else { tmp_r=decr(); tmp_l=c ; } x = tmp_l - tmp_r ; where anybool is simply declared as: /*@ assigns \nothing ; */ int anybool () ; However, this last approach may lead to an explosion of proof obligations.
TagsNo tags attached.
Attached Filesc file icon nondetexp_KO.c [^] (321 bytes) 2009-10-19 14:37 [Show Content]

- Relationships

-  Notes
virgile (developer)
2009-10-20 10:48

Unspecified evaluation order is already treated at the intra-function level with the -warn-unspecified-order of the value analysis. Inter-function level (such as is the case here) is on the TODO list.

- Issue History
Date Modified Username Field Change
2009-10-19 14:37 Sylvain Boulme New Issue
2009-10-19 14:37 Sylvain Boulme File Added: nondetexp_KO.c
2009-10-20 10:48 virgile Note Added: 0000470
2009-10-20 10:48 virgile Assigned To => virgile
2009-10-20 10:48 virgile Status new => acknowledged
2009-11-10 10:09 virgile Relationship added child of 0000070
2010-06-09 18:09 svn Checkin

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker