Frama-C Bug Tracking System - Frama-C
View Issue Details
0000289Frama-CPlug-in > jessiepublic2009-10-19 14:372010-06-09 18:09
Sylvain Boulme 
virgile 
normalmajoralways
acknowledgedopen 
Frama-C Beryllium-20090902 
 
0000289: unsoundness of Jessie with respect to expression evaluation of ANSI-C
The 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.
No tags attached.
c nondetexp_KO.c (321) 2009-10-19 14:37
https://bts.frama-c.com/file_download.php?file_id=23&type=bug
Issue History
2009-10-19 14:37Sylvain BoulmeNew Issue
2009-10-19 14:37Sylvain BoulmeFile Added: nondetexp_KO.c
2009-10-20 10:48virgileNote Added: 0000470
2009-10-20 10:48virgileAssigned To => virgile
2009-10-20 10:48virgileStatusnew => acknowledged
2009-11-10 10:09virgileRelationship addedchild of 0000070
2010-06-09 18:09svnCheckin

Notes
(0000470)
virgile   
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.