GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0000042	Frama-C	Plug-in > jessie	public	2009-04-07	2009-06-17

Reporter	virgile	Assigned To	cmarche	Resolution	open
Priority	normal	Severity	feature	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Lithium-20081201	Target Version	-	Fixed in Version	-

Description :

[bug 7561 from old bts, reported by Boris Hollas] For loops that loop on a variable i that is not decreased inside the loop a default loop invariant should be inferred.

For example, in

for(i=0; i<n; i++) { a[i] = 0; }

the loop invariant

//@ loop invariant 0 <= i;

should be inferred by default.

A similar loop invariant should be inferred for decreasing loops.