Assume loop conditions in loop bodies with sound loop havoc - #320

Problem

The verifier checked a loop body using values from before the loop. It could miss errors in later iterations and carry one iteration's facts past the loop. It also checked a for update before the body.

Example

int x = 3;
while (x > 0) {
    @Refinement("_ > 0") int y = x - 1; // Refinement Error
    x--;
}

Here x0, x1, etc. are symbolic versions of the same Java variable:

x0 = 3                       before the loop
x1 = fresh int               havoc before one arbitrary iteration; forget x0 = 3
assume x1 > 0                the guard holds on entry to the body
y = x1 - 1; require y > 0     fails when x1 = 1, because y = 0
x2 = x1 - 1                  the decrement, if checking continues
x3 = fresh int               havoc again after the loop

x1 = 1 is reachable: the successive loop-entry values are 3, 2, then 1. The previous verifier checked the body using the initial value 3 and accepted the program. The fresh x1 keeps only x's declared refinement, so this later iteration is now checked.

Change

• Havoc values the loop may change before and after checking one arbitrary iteration. Assume a while or for guard in the body when it has no direct variable writes.
• Check for initialization, condition, body, and update in execution order; account for continue. Handle do and for-each loops conservatively.
• Discard facts learned inside the loop afterward. We do not infer !guard after exit, since break can leave while the guard is true. This loses precision but avoids an invalid assumption.

Tests cover later iterations, guard facts, loop order, continue, break, fields, and typestate. mvn test passes.

Known existing limit: alias and this typestate changes can still be accepted incorrectly. This PR addresses the loop reasoning above; it does not establish soundness for those cases.

Fixes #306.