GeezerVison

Description

The verifier scanned the right operand of && and || as though it always ran. A write there could then be trusted after Java had skipped it. After checking the operator, this change gives each variable written in its right operand a fresh unconstrained value, so a refinement cannot rely on the skipped assignment.

This ports the paired reproducer and fix from closed #257 to current main. The test uses the current // Expect: convention and adds ||, nested assignments, increment, and a right operand without writes.

Example

int x = 0;
boolean ignored = false && ((x = 1) == 1);
@Refinement("_ == 1") int y = x; // Expect: Refinement Error

On main at dd02e996, the verifier accepts the expanded test file. This branch reports four expected refinement errors; the no-write case still passes. The original example fails its Java assertion when run with -ea.

This is conservative: it forgets a RHS write even when the left operand happens to force the RHS to run, so some safe code may need a more precise future path merge to verify.

Related Issue

Fixes #323. Based on 5d3f1c29 and c23f819d from #257; Guilherme Espada is credited in the commit.

Type of change

• Bug fix
• New feature
• Documentation update
• Code refactoring

Checklist

• Added tests under liquidjava-example/src/main/java/testSuite/
• mvn test passes locally
• Updated docs/README if behavior or API changed (not applicable)