Default invariant should be inferred for loops
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.