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

View Issue Details [ Jump to Notes ]

[ 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

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

Relationships

Notes

~0004563

correnson (manager)

2014-02-12 16:57

Fix committed to stable/neon branch.

Notes

Date Modified	Username	Field	Change
Issue History
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
2013-07-30 17:22	svn	Status	assigned => resolved
2013-07-30 17:22	svn	Resolution	open => fixed
2013-08-01 18:16	svn
2013-12-19 01:11		Source_changeset_attached	=> framac master 075a8446
2013-12-19 01:11	correnson	Source_changeset_attached	=> framac master 579331b2
2014-02-12 16:53		Source_changeset_attached	=> framac stable/neon 075a8446
2014-02-12 16:53	correnson	Source_changeset_attached	=> framac stable/neon 579331b2
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

Issue History