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 
PrioritynormalSeveritymajorReproducibilityalways
StatusacknowledgedResolutionopen 
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
(0000470)
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 - 2019 MantisBT Team
Powered by Mantis Bugtracker