Mention that invariant does not hold after for-loop
ID0000612: This issue was created automatically from Mantis Issue 612. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000612 | Frama-C | Documentation > ACSL | public | 2010-10-18 | 2014-02-12 |
| Reporter | Jochen | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | Frama-C Carbon-20101201-beta1 | Fixed in Version | Frama-C Carbon-20101201-beta1 |
Description :
The ACSL-1.4 reference, available from http://frama-c.com/acsl.html, explains on p.35-36 where the invariant of a for-loop shall hold as follows: ``The predicate I holds ... right after the initialization expression ...; for a for (init; c; step) s loop, I must be preserved by the side-effects of c followed by s followed by step''. While this is possibly the most compact explanation, it is based on the transformation of "for (init;c;step) s" into "init; while (1) { int C=c; if(!C) break; s; step; }", which seems to be rather unusual. As a consequence, the for-loop invariant does not hold after normal termination, if c has side-effects (cf. attached demonstration program). This unexpected fact should be mentioned in the ACSL reference.