Frama-C Bug Tracking System - Frama-C
View Issue Details
0000190Frama-CPlug-in > slicingpublic2009-07-15 12:012009-09-02 10:57
lukaszc 
patrick 
normalcrashalways
closedfixed 
 
Frama-C Beryllium-20090901 
0000190: crash when unbound variable
"frama-c -slice-rd y -pp-annot test.c" results in a crash ------------ test.c ------------ int x(int y, int z) { /*@ slice pragma expr y == 1; */ //@ assert y == 1; //@ assert y + z == 3; return 2*y*z1(); } int main() { x(1,2); return 0; } int z1() { return 1; }
No tags attached.
Issue History
2009-07-15 12:01lukaszcNew Issue
2009-07-15 12:01lukaszcStatusnew => assigned
2009-07-15 12:01lukaszcAssigned To => Anne
2009-07-15 13:07AnneNote Added: 0000257
2009-07-15 13:09AnneAssigned ToAnne => patrick
2009-07-15 13:09AnneNote Added: 0000258
2009-07-15 14:16patrickNote Added: 0000259
2009-07-15 14:20patrickNote Added: 0000260
2009-07-15 14:20patrickStatusassigned => resolved
2009-07-15 14:20patrickResolutionopen => fixed
2009-09-02 10:54signolesStatusresolved => closed
2009-09-02 10:57signolesFixed in Version => Frama-C Beryllium

Notes
(0000257)
Anne   
2009-07-15 13:07   
test file : tests/slicing/bts0190.c
(0000258)
Anne   
2009-07-15 13:09   
Patrick, I leave this one to you, beacause I don't know where is the best place to catch the exception.
(0000259)
patrick   
2009-07-15 14:16   
The raised exception comes from an error in the command line. The variable "y" isn't in the scope related to the -slicd-rd option: the end of the function selected as the entry point (the main function here). The correction is the following: catching the initial error exception to raise the Log.AbortError exception.
(0000260)
patrick   
2009-07-15 14:20   
correction of a crash coming from an user error