Impact: correct code is rejected with a syntax error: an array element written at an index that is not a variable or a literal (a[k++] = x, a[b.length - 1] = x). 4 of the 53 real-world files below.

Description

RefinementTypeChecker.visitCtArrayWrite turns the index expression into a refinement by parsing its source text (BuiltinFunctionPredicate.addToIndex(index.toString(), ...)). An index such as k++ or from.length - 1 is not a valid refinement expression, so the parser reports a syntax error on the user's code. to[k] = x and to[i] = x are fine. The index could be translated from its AST (as other expressions are), or left unconstrained when it cannot be.

Minimal reproducer

public class Repro {
    static int copy(String[] from, String[] to) {
        int k = 0;
        for (int i = 0; i < from.length; i++) {
            to[k++] = from[i];
        }
        return k;
    }
}

Expected

Correct! Passed Verification.

Actual

Syntax Error: Invalid refinement expression, expected a logical predicate
3 |         int k = 0;
4 |         for (int i = 0; i < from.length; i++) {
5 |             to[k++] = from[i];
  |             ^^^^^^^
6 |         }
7 |         return k;
Repro.java:5

The same error with to[from.length - 1] = from[i];. Reproduced on main at ad055b4 (liquidjava-verifier 0.0.35).

Real-world files that hit it

• newVal[oldVal.length] = (float) (...) — pacsbrasil/dcm4che2 (file)
• newVal[oldVal.length] = (float) (...) — fenyuzhe/protoss-toolkit (file)
• result[array.length-1-i] = array[i]; — hashsploit/clank (file)
• urls[k++] = u; — larael/javacpp (file)

Context

Found while running LiquidJava on the original repository files of 53 real-world typestate and refinement bugs (the files our study exercises were simplified from). The error is reported on code with no refinement of its own, so it is a false error in every file that has the construct. Related: #348 (a[i].length, also a false syntax error, from a different place).