2021-01-22 20:45 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000612Frama-CDocumentation > ACSLpublic2014-02-12 16:55
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytextReproducibilityN/A
StatusclosedResolutionfixed 
Product VersionFrama-C Boron-20100401 
Target VersionFrama-C Carbon-20101201-beta1Fixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000612: Mention that invariant does not hold after for-loop
DescriptionThe 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.
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (1,103 bytes) 2010-10-18 17:48 -
    /*
     * This program demonstrates that a loop invariant need not hold after
     * normal termination of a for-loop, if its condition has side-effects.
     * 
     * The global variable j is treated in the same way as 
     * the local (to main()) variable i:
     * both are initialized to 0 (line 41, 46),
     * and then incremented repeatedly in the loop (line 34/46, 46).
     * 
     * In fact, the invariant j==i can be proven (line 44).
     * 
     * However, right after the loop, an unsatisfiable obligation of the form
     * "(...something satisfiable...) ==> i+1 == i"
     * is generated for the assert in line 48.
     * 
     * In fact, "i=5 j=6" is printed to stdout,
     * when the #include and the printf is uncommented.
     */
    
    
    
    //#include <stdio.h>
    
    static int j;
    
    /*@ requires j < 100;
        assigns j;
        ensures j == \old(j) + 1;
        ensures \result == x;
    */
    static int f(int x)
    {
        ++j;
        return x;
    }
    
    int main(void)
    {
        int i;
        j = 0;
        /*@ loop variant 5 - i;
    	loop invariant 0 <= i <= 5;
    	loop invariant j == i;
        */
        for (i=0; f(i)<5; ++i)
    	;
        /*@ assert j == i; */
        //printf("i=%d j=%d\n",i,j);
        return 0;
    }
    
    
    c file icon ftest.c (1,103 bytes) 2010-10-18 17:48 +

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2010-10-18 17:48 Jochen New Issue
2010-10-18 17:48 Jochen Status new => assigned
2010-10-18 17:48 Jochen Assigned To => signoles
2010-10-18 17:48 Jochen File Added: ftest.c
2010-10-18 18:01 signoles Assigned To signoles => virgile
2010-10-26 13:12 virgile Target Version => Frama-C Carbon
2010-12-02 16:54 svn
2010-12-02 16:54 svn Status assigned => resolved
2010-12-02 16:54 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:35 signoles Status resolved => closed
2013-12-19 01:12 Source_changeset_attached => framac master d592363e
2014-02-12 16:55 Source_changeset_attached => framac stable/neon d592363e
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
+Issue History