Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000186Frama-CPlug-in > slicingpublic2009-07-14 14:302014-02-12 16:56
Reporterlukaszc 
Assigned ToAnne 
PriorityhighSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090601-beta1 
Target VersionFrama-C Boron-20100401Fixed in VersionFrama-C Boron-20100401 
Summary0000186: Stack overflow when slicing functions invoking themselves circularily
DescriptionStack overflow for the following code: /*@ requires y == 1; @ ensures @ \result == 2*y; @*/ int x(int y, int z) { //@ assert y == 1; //@ assert y + z == 3; return 2*y*z1(); } int main() { x(1,2); return 0; } int z1() { return x(2,2); }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000248)
lukaszc (reporter)
2009-07-14 14:31

invoked with -slice-return x
(0000256)
Anne (reporter)
2009-07-15 13:06

test file : tests/slicing/bts0186.c
(0000422)
Anne (reporter)
2009-09-29 13:50

Due to stupid propagations of empty selections... try to remove them !

- Issue History
Date Modified Username Field Change
2009-07-14 14:30 lukaszc New Issue
2009-07-14 14:30 lukaszc Status new => assigned
2009-07-14 14:30 lukaszc Assigned To => Anne
2009-07-14 14:31 lukaszc Note Added: 0000248
2009-07-15 13:06 Anne Note Added: 0000256
2009-08-26 11:42 Anne Status assigned => acknowledged
2009-09-23 20:23 signoles Priority normal => high
2009-09-23 20:23 signoles Target Version => Frama-C Bore
2009-09-29 13:50 Anne Note Added: 0000422
2009-09-29 13:55 svn Checkin
2009-09-29 13:55 svn Status acknowledged => resolved
2009-09-29 13:55 svn Resolution open => fixed
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version => Frama-C Boron


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker