Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000685Frama-CKernelpublic2011-01-24 15:082012-09-19 17:16
Reportervirgile 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000685: CIL's added return masks issues
DescriptionWhen 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;
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001419)
virgile (developer)
2011-01-24 15:11

Frama-C should generate /*@ assert \false; */ in addition to return 0;
(0003080)
yakobowski (manager)
2012-06-09 23:16

Fixed by Virgile in revision 17366

- Issue History
Date Modified Username Field Change
2011-01-24 15:08 virgile New Issue
2011-01-24 15:08 virgile Status new => assigned
2011-01-24 15:08 virgile Assigned To => virgile
2011-01-24 15:11 virgile Note Added: 0001419
2012-06-09 23:16 yakobowski Note Added: 0003080
2012-06-09 23:16 yakobowski Status assigned => resolved
2012-06-09 23:16 yakobowski Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker