assigns, loop assigns and loop invariant

ID0001461: This issue was created automatically from Mantis Issue 1461. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001461	Frama-C	Plug-in > wp	public	2013-07-24	2014-06-17

Reporter	virgile	Assigned To	correnson	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	-

Description :

In the following (admittedly contrived) example, the assigns of g is not proved by WP (in fact it is reduced to false by Qed), although it is correct from ACSL semantics: as long as the loop invariant states that x still has its old value, the fact that it is mentioned in the loop assigns should not impede its absence in the assigns.

--- test.c

int x;

/*@ assigns \nothing; */
int g() {
  /*@ loop assigns i,x;
      loop invariant x == \at(x,Pre);
  */
  for (int i = 0; i<2; i++);
  return x;
}

Steps To Reproduce :

frama-c -wp test.c