Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001632Frama-CKernel > ACSL implementationpublic2014-01-27 09:212014-10-29 11:05
Reportervirgile 
Assigned Tovirgile 
PrioritylowSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0001632: Translation of abrupt clause into assert do not take 'for :' clause into account
DescriptionIn the program written given below, the returns clause is translated into two assert that are not related to the foo behavior, resulting in an unprovable assertion in the else branch.
Steps To Reproduce/*@ behavior foo:
  assumes a == 0;
*/
int foo(int a) {
  /*@ for foo:
    returns \result == 0;
  */
  { if (a==0) { return 0; }
    else return 2;
  }
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-01-27 09:21 virgile New Issue
2014-01-27 09:21 virgile Status new => assigned
2014-01-27 09:21 virgile Assigned To => virgile
2014-10-29 11:05 rajshukla Tag Attached: Windows
2014-10-29 11:05 rajshukla Tag Attached: csmith
2014-10-29 11:05 rajshukla Tag Detached: Windows
2014-10-29 11:05 rajshukla Tag Detached: csmith


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker