[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: nextInt(dec(size())) gives size()¹⁹ >= 0 && dec(size())²¹ == size()¹⁹ - 1 is not a subtype of dec(size())²¹ > 0. An unrefined call reads plain()⁸ == #plain_result⁷ (result name from #483).

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)), field reads (bound == this.f), other expressions (bound == this.f - 1) and literals keep the parameter name: their refinement is bound == <their code>, so writing them as code would read as a tautology (0 == 0, which TestGeneratedNames would catch).

How

Same approach as FieldDisplayNames (#459): MethodsFunctionsChecker records the call's source text as written (Spoon's original source fragment, so count() is not printed as Basket.count()) for the argument instance in the new ArgumentDisplayNames. VariableFormatter.format writes it with the counter, and ExpressionNameResolver keeps it whole, as it does for fields (items.size() is not cut to size()). A call with no source position (built by Spoon, not read from a file) keeps the parameter name. CommandLineLauncher clears the record at the start of each run. The internal name and the SMT query are unchanged.

Size

+68 / −7 over 7 files (main code +48 / −2; the new ArgumentDisplayNames is 35 of those lines, most of them Javadoc).

Tests

• TestFoundBinders: the reproducer's rows (also in the original step of the history) now use items.size(); new callArgumentIsWrittenAsTheCallerWroteIt on a new fixture line random.nextInt(count()), checking the message and counterexample read count(), not bound or Basket.count().
• All of them fail on main, and the rows fail without the ExpressionNameResolver change.
• mvn test: 693 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.

[CatarinaGamboa]

Codex review, round 5 (after rebasing on #483 and #484)

• [P2] MethodsFunctionsChecker.java:465 — An invocation argument without a source position can crash verification here. Spoon returns a no-source fragment in that case, so reading its source code is unsafe. Check for a usable fragment and fall back to iArg.toString() for display.

[CatarinaGamboa]

Codex review, round 5: response

• Fixed, differently: a call argument with no source position (one Spoon builds itself rather than reading from a file) is no longer renamed and keeps the parameter name. Falling back to iArg.toString() would print Spoon's form (Basket.count()), which is not what the caller wrote either. Amended into the single commit.