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 - 2018 MantisBT Team
Powered by Mantis Bugtracker