Frama-C Bug Tracking System - Frama-C
View Issue Details
0000289Frama-CPlug-in > jessiepublic2009-10-19 14:372010-06-09 18:09
Sylvain Boulme 
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
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

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.