Frama-C Bug Tracking System - Frama-C
View Issue Details
0000685Frama-CKernelpublic2011-01-24 15:082012-09-19 17:16
virgile 
virgile 
normalfeaturealways
closedfixed 
Frama-C Carbon-20101202-beta2 
Frama-C Oxygen-20120901 
0000685: CIL's added return masks issues
When an execution path in a function may fall through, CIL adds automatically a return statement. If the path is not unfeasible, this would mask an undefined behavior (6.9.1.14), as shown in the example below, where Frama-C would conclude that z is 0, while gcc reports 12: int x; int f(void) { x++; if (x<=10) return x-1; } int main() { x = 11; int y = 42; int z = f(); return z; }
No tags attached.
Issue History
2011-01-24 15:08virgileNew Issue
2011-01-24 15:08virgileStatusnew => assigned
2011-01-24 15:08virgileAssigned To => virgile
2011-01-24 15:11virgileNote Added: 0001419
2012-06-09 23:16yakobowskiNote Added: 0003080
2012-06-09 23:16yakobowskiStatusassigned => resolved
2012-06-09 23:16yakobowskiResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed

Notes
(0001419)
virgile   
2011-01-24 15:11   
Frama-C should generate /*@ assert \false; */ in addition to return 0;
(0003080)
yakobowski   
2012-06-09 23:16   
Fixed by Virgile in revision 17366