Frama-C Bug Tracking System - Frama-C
View Issue Details
0001462Frama-CPlug-in > wppublic2013-07-29 14:482014-03-13 15:57
virgile 
correnson 
normalmajoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Neon-20140301 
0001462: invalid loop invariant marked as valid (without pending hypothesis)
Given 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.
frama-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
-- 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; */ }
}
No tags attached.
Issue History
2013-07-29 14:48virgileNew Issue
2013-07-29 14:48virgileStatusnew => assigned
2013-07-29 14:48virgileAssigned To => correnson
2013-07-29 14:49virgileRelationship addedrelated to 0001353
2013-07-29 14:59virgileRelationship deletedrelated to 0001353
2013-07-30 17:22svnCheckin
2013-07-30 17:22svnStatusassigned => resolved
2013-07-30 17:22svnResolutionopen => fixed
2013-08-01 18:16svnCheckin
2014-02-12 16:57corrensonNote Added: 0004563
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004563)
correnson   
2014-02-12 16:57   
Fix committed to stable/neon branch.