Write a call argument as the caller wrote it in refinement errors

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());