[CatarinaGamboa]

Problem

When a call argument is itself a call, the refinement error named its value after the callee's parameter (bound), which is not in the caller's code.

Before / after

Issue reproducer (return nextInt(size());):

before: bound³ >= 0 is not a subtype of bound³ > 0
        Counterexample: bound³ == 0
after:  size()³ >= 0 is not a subtype of size()³ > 0
        Counterexample: size()³ == 0

Real case, fixture classes/found_binders_error (random.nextInt(items.size()), as in chaos-http-proxy's failures.size()):

before: bound⁶ == size(this.items) && bound⁶ >= 0 is not a subtype of bound⁶ > 0
        ∀bound⁶   bound⁶ == size(this.items) && bound⁶ >= 0
        Counterexample: bound⁶ == 0
after:  items.size()⁶ == size(this.items) && items.size()⁶ >= 0 is not a subtype of items.size()⁶ > 0
        ∀items.size()⁶   items.size()⁶ == size(this.items) && items.size()⁶ >= 0
        Counterexample: items.size()⁶ == 0

Nested calls read the same way: nextInt(dec(size())) gives size()¹⁹ >= 0 && dec(size())²¹ == size()¹⁹ - 1 is not a subtype of dec(size())²¹ > 0.

The argument keeps its instance counter, like every other instance, so two calls written alike (between(next(), next())) stay apart.

Unchanged

• Plain variables (positive(t) → t), field reads (bound == this.f), other expressions (bound == this.f - 1) and literals keep the parameter name. Their refinement is bound == <expression>, so naming them after the expression would read as a tautology (this.f == this.f).
• A call whose refinement only ties it to its result variable (an unrefined method: bound == plain⁷) also keeps it, for the same reason.

How

Same approach as FieldDisplayNames (#459): MethodsFunctionsChecker records the call's source text (Utils.getSourceCode, so size() stays size() instead of Spoon's Probe.size()) for the argument instance in the new ArgumentDisplayNames. VariableFormatter.format writes that text, and ExpressionNameResolver keeps it whole, as it does for fields (items.size() is not cut to size()). CommandLineLauncher clears the record at the start of each run. The internal name and the SMT query are unchanged.

Tests

• TestFoundBinders: the reproducer's message, row and counterexample now use items.size(); also the original step in the history.
• ExpressionNameResolverTest.writesACallArgumentAsTheCallerWroteIt.
• mvn test: 692 tests, 0 failures.

Closes #481

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

• [P2] Utils.java:190 — replaceAll("\\s+", " ") changes whitespace inside string literals and text blocks. A call such as check("a b") will appear in diagnostics as check("a b"), which is different source code. Collapse whitespace only outside literals, or preserve the source slice as written.

[CatarinaGamboa]

Codex review, round 1: response

• Fixed: whitespace collapsing. Utils.getSourceCode now only joins the lines of a multi-line argument (a line break and the indentation around it become one space), so spacing inside string literals is kept. A text block argument still has its lines joined, which is needed to show it on one line.

[CatarinaGamboa]

Codex review, round 2

• [P2] MethodsFunctionsChecker.java:468 — Distinct calls with identical source text receive the same display name. For example, two next() arguments can be separate values to the verifier but both appear as next() in a failed precondition or counterexample, producing misleading output such as next() < next(). Keep an occurrence marker or instance suffix when the display names collide.

[CatarinaGamboa]

Codex review, round 2: response

• Fixed: calls written alike. The argument now keeps its instance counter like every other instance (size()³ >= 0 is not a subtype of size()³ > 0), so between(next(), next()) shows next()⁴ and next()⁶. The PR description is updated with the new messages.

[CatarinaGamboa]

Codex review, round 3

• [P2] Utils.java:188 — Joining every source line also joins lines inside a Java text block passed to a call. The displayed binder and counterexample can therefore show different text from the argument the caller wrote. Preserve literal contents when formatting the snippet.

[CatarinaGamboa]

Codex review, round 3: response

• Declined: text blocks inside a call argument. Message rows, binders and counterexamples are one line each, so a multi-line argument has to be joined to be shown at all; keeping a text block's line breaks would break the row layout. Only the line breaks change, never the characters on a line, and a text block passed to a refined call inside another call's argument is rare. No code change this round.

[CatarinaGamboa]

Codex review, round 4

Nothing relevant found. The new argument names affect diagnostic formatting only; no change to the verifier's proof obligations and no concrete correctness issue.