Soundness: after a loop, the state is taken from the loop body as if it ran at least once

[CatarinaGamboa]

Impact: a real bug passes verification (false negative). It blocks 1 of the 48 real-code examples we built (bugs mined from open-source Java).

Description

A state set only inside a while body is assumed after the loop, although the loop may run zero times. reset() after a loop that is the only place mark() is called passes; with an if instead of the loop it is reported (control). Related to #306 (loop condition inside the body), but a different problem: tested against PR #320 (3edab83), which does not change it.

Minimal reproducer

import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

@StateSet({"open", "marked"})
class Buf {
    @StateRefinement(to = "open(this)")
    public Buf() {}

    @StateRefinement(to = "marked(this)")
    public void mark() {}

    @StateRefinement(from = "marked(this)", to = "open(this)")
    public void reset() {}
}

public class Repro {
    static void rewind(int n) {
        Buf b = new Buf();
        int k = 0;
        while (k < n) {
            b.mark();
            k++;
        }
        b.reset();          // with n == 0 the loop never runs and b was never marked
    }
}

Expected

A state error at b.reset(): the state after the loop is the join of the state before the loop and after the body (open(b) || marked(b)).

Actual

Correct! Passed Verification.

Control: the same code without the problem construct is reported

import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

@StateSet({"open", "marked"})
class Buf {
    @StateRefinement(to = "open(this)")
    public Buf() {}

    @StateRefinement(to = "marked(this)")
    public void mark() {}

    @StateRefinement(from = "marked(this)", to = "open(this)")
    public void reset() {}
}

public class Control {
    static void rewind(int n) {
        Buf b = new Buf();
        if (n > 0) {
            b.mark();
        }
        b.reset();          // the same with an if: reported
    }
}

State Refinement Error: found n > 0 ? marked(b¹¹) : open(b¹¹) but expected marked(b¹¹)
20 |             b.mark();
21 |         }
22 |         b.reset();          // the same with an if: reported
   |         ^^^^^^^^^^
23 |     }

Reproduced on main at 0472025 (liquidjava-verifier 0.0.35); also on fbfb4e2 and 0.0.33 in the original form. Related: #306, PR #320.

Context

Found while turning bugs mined from real open-source Java (fixed upstream or still present) into study examples for the error-message study.