Soundness bug: Assignable treatment is wrong

[mattulbrich]

Description

false can be proved exploiting a problem in the faulty assignable treatment of loops.

Reproducible

always. Example attached

Steps to reproduce

Load the attached proof for the follwoing example:

problem.zproof.gz
(github does no longer accept .zproof files, so you have to gunzip this.)

class A {
    
    /*@ normal_behaviour
      @  requires a.length == 2;
      @  ensures \result == 0;
      @ also
      @ normal_behaviour
      @  requires a.length == 2;
      @  ensures \result == 1;
      @*/
    int problem(int[] a) {
        int i = 0;
        a[1] = 0;
        /*@ loop_invariant 0<=i<=1;
          @ loop_invariant i == 0 ==> a[1] == 0;
          @ loop_invariant a[0] == \old(a[0]);
          @ decreases 2-i;
          @ assignable a[i];
          @*/
        while(i < 1) {
            i++;
            a[1] = 1;
        }
        return a[1];
    }

    /*@ normal_behaviour
      @  ensures b;
      @*/
    void proveAnything(boolean b) {
        int r = problem(new int[2]);
        //@ assert r == 0;
        //@ assert r == 1;
    }

    /*@ normal_behaviour
      @  ensures false;
      @*/
    void proveFalse() {
        proveAnything(false);
    }
}

Additional information

The problem is that in the PO for loop preservation the wrong variable value is used in the evaluation of assignable clauses.

---

• Commit: 8077951