Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001462Frama-CPlug-in > wppublic2013-07-29 14:482014-03-13 15:57
Reportervirgile 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001462: invalid loop invariant marked as valid (without pending hypothesis)
DescriptionGiven the program below, wp discharges all proof obligations, including the first loop invariant whose preservation is false. This allows then to prove the invalid assertion after the loop. It seems that all three loop invariants (with their \at() term) are necessary to reproduce the issue.
Steps To Reproduceframa-c -wp file.c
One can see the inconsistent status (green/black bullet) of the assert with
frama-c-gui -wp file.c -then -val -main f -slevel 100
Additional Information-- file.c
void f(int c) {
  int x = 0;
  int y = 0;
  /*@ assert for_value: c<= 0 || c == 1 || c>=2; */
  if (c==2) { x=1; y=1; }
 L:
  /*@
    loop invariant \at(x==0,L) ==> i!=0 ==> y == 0;
    loop invariant \at(x==1,L) ==> i!=0 ==> x == 1;
    loop invariant \at(c==0,Pre) ==> i==0 ==> x == 0;
    loop assigns i,x,y;
   */
  for (int i = 0; i<10; i++) {
    if (c == 0) { x = 0; }
    if (c == 1) { y = 1; }
    if (c == 2) { x = 1; }
  }
  if (c==1) { /*@ assert consequence_of_false_invariant: y==0; */ }
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004563)
correnson (manager)
2014-02-12 16:57

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2013-07-29 14:48 virgile New Issue
2013-07-29 14:48 virgile Status new => assigned
2013-07-29 14:48 virgile Assigned To => correnson
2013-07-29 14:49 virgile Relationship added related to 0001353
2013-07-29 14:59 virgile Relationship deleted related to 0001353
2013-07-30 17:22 svn Checkin
2013-07-30 17:22 svn Status assigned => resolved
2013-07-30 17:22 svn Resolution open => fixed
2013-08-01 18:16 svn Checkin
2014-02-12 16:57 correnson Note Added: 0004563
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker