Frama-C Bug Tracking System - Frama-C
View Issue Details
0000184Frama-CPlug-in > slicingpublic2009-07-14 14:132014-02-12 16:57
lukaszc 
Anne 
normalcrashalways
closedfixed 
Frama-C Beryllium-20090601-beta1 
Frama-C Beryllium-20090901 
0000184: slicing crashes when there is no entry point to the function
frama-c -slice-pragma x file.c file.c ----- int x(int y, int z) { /*@ slice pragma expr y == 1; */ //@ assert y == 1; //@ assert y + z == 3; return y; } int main() { return 0; } int z1() { return x(2,2); }
No tags attached.
Issue History
2009-07-14 14:13lukaszcNew Issue
2009-07-14 14:13lukaszcStatusnew => assigned
2009-07-14 14:13lukaszcAssigned To => Anne
2009-07-15 09:44svnCheckin
2009-07-15 09:51svnCheckin
2009-07-15 09:51svnStatusassigned => resolved
2009-07-15 09:51svnResolutionopen => fixed
2009-09-02 10:54signolesStatusresolved => closed
2009-09-02 10:57signolesFixed in Version => Frama-C Beryllium

There are no notes attached to this issue.