0001462: invalid loop invariant marked as valid (without pending hypothesis)

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001462

Frama-C

Plug-in > wp

public

2013-07-29 14:48

2014-03-13 15:57

Reporter

virgile

Assigned To

correnson

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Neon-20140301

Summary

0001462: invalid loop invariant marked as valid (without pending hypothesis)

Description

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.

Steps To Reproduce

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

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; */ }
}

Tags

No 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