Look up spread varargs calls by declared arity in operations and loops

Arithmetic operands and loop havoc looked methods up by the call's argument
count, so a call that spreads its varargs missed the declaration: its return
refinement was lost inside an expression, and a typestate-changing varargs
call in a loop did not havoc its receiver, letting a post-loop state
violation pass. Both now use the number of parameters the method declares.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java

@@ -16,6 +16,11 @@ static int pick(@Refinement("k >= 0") int k, int... xs) {
         return k;
     }
 
+    @Refinement("_ == 7")
+    static int seven(int... xs) {
+        return 7;
+    }
+
     CorrectVarargsCall(@Refinement("length(xs) > 1") int... xs) {
     }
 
@@ -30,6 +35,8 @@ public static void main(String[] args) {
         int h = pick(0);
         int i = pick(1, 2, 3);
         int j = count("a", "b") + 1;
+        @Refinement("_ == 8")
+        int k = seven(1, 2) + 1;
         new CorrectVarargsCall(1, 2);
     }
 }

liquidjava-example/src/main/java/testSuite/ErrorVarargsLoopState.java

@@ -0,0 +1,27 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "marked"})
+public class ErrorVarargsLoopState {
+    @StateRefinement(to = "open(this)")
+    ErrorVarargsLoopState() {}
+
+    @StateRefinement(to = "marked(this)")
+    void mark(int... tags) {}
+
+    @StateRefinement(from = "marked(this)", to = "open(this)")
+    void reset() {}
+
+    // The loop may run zero times, leaving b open, even when mark spreads its varargs.
+    static void mayBeEmpty(int n) {
+        ErrorVarargsLoopState b = new ErrorVarargsLoopState();
+        int k = 0;
+        while (k < n) {
+            b.mark(1, 2);
+            k++;
+        }
+        b.reset(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -677,7 +677,7 @@ private void havocChangedIn(CtLoop loop) {
         Set<String> names = new LinkedHashSet<>();
         for (CtAbstractInvocation<?> call : calls) {
             if (call instanceof CtInvocation<?> inv
-                    && context.getAllMethodsWithNameSize(inv.getExecutable().getSimpleName(), inv.getArguments().size())
+                    && context.getAllMethodsWithNameSize(inv.getExecutable().getSimpleName(), Utils.declaredArity(inv))
                             .stream().anyMatch(f -> f.getAllStates().stream().anyMatch(ObjectState::hasTo))) {
                 if (inv.getTarget()instanceof CtVariableAccess<?> target)
                     changed.add(target);

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

@@ -275,7 +275,8 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
 
             // Get function refinements with non_used variables
             String met = method.getParent(CtType.class).getQualifiedName(); // TODO check
-            RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met, inv.getArguments().size());
+            RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met,
+                    method.getParameters().size());
             if (fi == null)
                 return getUnconstrainedInvocationVariable(inv);
             Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!!
@@ -313,7 +314,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv) thr
             String typeNotParametrized = (i > 0) ? c.substring(0, i) : c;
             String methodInClassName = typeNotParametrized + "." + simpleName;
             RefinedFunction fi = rtc.getContext().getFunction(methodInClassName, typeNotParametrized,
-                    inv.getArguments().size());
+                    Utils.declaredArity(inv));
             if (fi == null)
                 return getUnconstrainedInvocationVariable(inv);
             Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!!

liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

@@ -8,6 +8,7 @@
 import java.util.stream.Stream;
 
 import liquidjava.utils.constants.Types;
+import spoon.reflect.code.CtAbstractInvocation;
 import spoon.reflect.code.CtBlock;
 import spoon.reflect.code.CtFor;
 import spoon.reflect.code.CtForEach;
@@ -18,6 +19,7 @@
 import spoon.reflect.declaration.CtAnnotation;
 import spoon.reflect.declaration.CtConstructor;
 import spoon.reflect.declaration.CtElement;
+import spoon.reflect.declaration.CtExecutable;
 import spoon.reflect.declaration.CtMethod;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtFieldReference;
@@ -56,6 +58,15 @@ public static String qualifyFieldName(CtFieldReference<?> field) {
         return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName();
     }
 
+    /**
+     * Number of parameters the invoked method declares, which differs from the number of arguments when a call spreads
+     * its varargs
+     */
+    public static int declaredArity(CtAbstractInvocation<?> invocation) {
+        CtExecutable<?> method = invocation.getExecutable().getExecutableDeclaration();
+        return method != null ? method.getParameters().size() : invocation.getExecutable().getParameters().size();
+    }
+
     public static String getFile(CtElement element) {
         SourcePosition pos = element.getPosition();
         if (pos == null || pos.getFile() == null)