Write a call argument as the caller wrote it in refinement errors (#486)

## 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](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java

@@ -68,4 +68,14 @@ void addUp(int first, int second) {
     void forward(int t) {
         positive(t); // Expect: Refinement Error
     }
+
+    @Refinement("_ >= 0")
+    static int count() {
+        return 0;
+    }
+
+    // a call argument is written as the caller wrote it, not as the callee's parameter
+    int pickByCount() {
+        return random.nextInt(count()); // Expect: Refinement Error
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java

@@ -9,6 +9,7 @@
 import liquidjava.diagnostics.warnings.CustomWarning;
 import liquidjava.processor.RefinementProcessor;
 import liquidjava.processor.context.ContextHistory;
+import liquidjava.rj_language.ast.formatter.ArgumentDisplayNames;
 import liquidjava.rj_language.ast.formatter.FieldDisplayNames;
 import liquidjava.specification.Refinement;
 import picocli.CommandLine;
@@ -59,6 +60,7 @@ public static void launch(String... paths) {
         diagnostics.clear();
         contextHistory.clearHistory();
         FieldDisplayNames.clear();
+        ArgumentDisplayNames.clear();
         Launcher launcher = new Launcher();
         for (String path : paths) {
             if (!new File(path).exists()) {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -16,6 +16,7 @@
 import liquidjava.processor.refinement_checker.object_checkers.AuxHierarchyRefinementsPassage;
 import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.formatter.ArgumentDisplayNames;
 import liquidjava.utils.GeneratedNames;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
@@ -459,6 +460,10 @@ private String createVariableRepresentingArgument(CtExpression<?> iArg, Variable
             met = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), met);
         String nVar = String.format(Formats.INSTANCE, fArg.getName(), rtc.getContext().getCounter());
         rtc.getContext().addInstanceToContext(nVar, fArg.getType(), met.substituteVariable(Keys.WILDCARD, nVar), iArg);
+        // a call in the source reads as written; any other argument is refined as equal to its code, which would read
+        // as a tautology
+        if (iArg instanceof CtInvocation && iArg.getPosition().isValidPosition())
+            ArgumentDisplayNames.recordArgument(nVar, iArg.getOriginalSourceFragment().getSourceCode());
         return nVar;
     }
 

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ArgumentDisplayNames.java

@@ -0,0 +1,35 @@
+package liquidjava.rj_language.ast.formatter;
+
+import java.util.Map;
+import java.util.concurrent.ConcurrentHashMap;
+
+/**
+ * The code of the call arguments that a verification names after the callee's parameter, so that
+ * {@link VariableFormatter} can write such an argument as the caller wrote it ({@code items.size()} rather than
+ * {@code bound}). Filled during a verification and cleared when the next one starts
+ */
+public final class ArgumentDisplayNames {
+    private static final Map<String, String> ARGUMENTS = new ConcurrentHashMap<>();
+
+    private ArgumentDisplayNames() {
+    }
+
+    /**
+     * Records that an argument instance ({@code #<parameter>_<n>}) stands for the argument {@code code}. Only the
+     * display changes
+     */
+    public static void recordArgument(String instanceName, String code) {
+        ARGUMENTS.put(instanceName, code);
+    }
+
+    /**
+     * Forgets what the previous verification recorded
+     */
+    public static void clear() {
+        ARGUMENTS.clear();
+    }
+
+    static String argumentCode(String instanceName) {
+        return ARGUMENTS.get(instanceName);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java

@@ -22,8 +22,8 @@ public static ExpressionNameResolver forExpression(Expression expression) {
 
     public String resolveVariable(String name) {
         String formatted = VariableFormatter.format(name);
-        // a field is always written as in code, as its binder and the counterexample write it
-        if (VariableFormatter.isField(name))
+        // a field or call argument is always written as in code, as its binder and the counterexample write it
+        if (VariableFormatter.isField(name) || ArgumentDisplayNames.argumentCode(name) != null)
             return formatted;
         return isAmbiguous(name, variables, ExpressionNameResolver::getVariableSimpleName) ? formatted
                 : Utils.getSimpleName(formatted);

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java

@@ -25,6 +25,10 @@ public static String format(String name) {
 
         String baseName = matcher.group(1);
         String counter = matcher.group(2);
+        // the counter tells apart calls written alike, which can return different values
+        String argument = ArgumentDisplayNames.argumentCode(name);
+        if (argument != null)
+            return argument + toSuperscript(counter);
         String receiver = FieldDisplayNames.writeReceiver(name);
         if (receiver != null && isField(baseName))
             return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + toSuperscript(counter);

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java

@@ -57,16 +57,21 @@ static void verify() {
     @Test
     void issueReproducerDropsTheTrueFieldRow() {
         Shown shown = ERRORS.get(25);
-        assertEquals(List.of("∀bound bound == size(this.items) && bound >= 0"), shown.rows());
-        assertEquals("bound == size(this.items) && bound >= 0 is not a subtype of bound > 0", shown.message());
+        assertEquals(List.of("∀items.size() items.size() == size(this.items) && items.size() >= 0"), shown.rows());
+    }
+
+    @Test
+    void callArgumentIsWrittenAsTheCallerWroteIt() {
+        Shown shown = ERRORS.get(79);
+        assertEquals("count() >= 0 is not a subtype of count() > 0", shown.message());
+        assertEquals("Counterexample: count() == 0", shown.counterexample());
     }
 
     @Test
     void steppingBackReachesTheOriginalWithTheDroppedRow() {
         Shown shown = ERRORS.get(25);
-        assertEquals(
-                List.of("∀this.items true", "∀items items == this.items", "∀bound bound == size(items) && bound >= 0"),
-                shown.originalRows());
+        assertEquals(List.of("∀this.items true", "∀items items == this.items",
+                "∀items.size() items.size() == size(items) && items.size() >= 0"), shown.originalRows());
         assertEquals(List.of("Substitution", "Binder"), shown.steps());
         assertEquals(List.of("this#testSuite.classes.found_binders_error.Basket.items", "#items_", "#bound_"),
                 shown.originalBinders());