2021-02-24 18:28 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000452Frama-CKernelpublic2014-02-12 16:55
Reporteryakobowski 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000452: "Body of function main falls-through" warning could be improved
DescriptionIn the following code (seen in the wild...), the 'break' after 'return 0' causes frama-C to think that the switch sometimes does not return a value.

int main (int foo, char** args) {
  switch(foo) {
  case 1:
    return 0;
    break;

  default:
    return 1;
  }
}
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2010-04-13 11:45 yakobowski New Issue
2010-04-13 11:46 signoles Status new => assigned
2010-04-13 11:46 signoles Assigned To => virgile
2010-05-31 15:11 svn
2010-05-31 15:12 virgile Status assigned => resolved
2010-05-31 15:12 virgile Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed
2013-12-19 01:13 Source_changeset_attached => framac master 4710ae57
2014-02-12 16:55 Source_changeset_attached => framac stable/neon 4710ae57
+Issue History