From 3e3aac3c4812059b399998f40f758c6e69391536 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 13 Oct 2026 09:56:58 +0100 Subject: [PATCH 1/4] Leave the length of unnamed array expressions unrefined (#348) A `.length` read was translated to the refinement `_ == length()` by printing the target expression into the refinement string, so any target other than a plain name (`grid[i]`, `o.arr()`, `this.arr`, `r.arr`) produced a string the refinement parser rejects, reported as "Syntax Error: Invalid refinement expression" on code with no refinements at all. Only a local variable or parameter can be named in a refinement, so only those keep the `length(x)` refinement; the length of any other array expression is now an unconstrained int, which is sound (it can only lose information). Fixes #348 Co-Authored-By: Claude Opus 5.5 --- .../CorrectLengthOfArrayExpression.java | 36 +++++++++++++++++++ .../ErrorLengthOfArrayExpression.java | 14 ++++++++ .../RefinementTypeChecker.java | 11 ++++-- 3 files changed, 58 insertions(+), 3 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectLengthOfArrayExpression.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLengthOfArrayExpression.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLengthOfArrayExpression.java b/liquidjava-example/src/main/java/testSuite/CorrectLengthOfArrayExpression.java new file mode 100644 index 00000000..33b69559 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectLengthOfArrayExpression.java @@ -0,0 +1,36 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class CorrectLengthOfArrayExpression { + + int[] values = new int[3]; + + int[] values() { + return values; + } + + static double sum(double[][] grid) { + double total = 0; + for (int i = 0; i < grid.length; i++) { + for (int j = 0; j < grid[i].length; j++) { + total += grid[i][j]; + } + } + return total; + } + + static int sizes(CorrectLengthOfArrayExpression o) { + return o.values().length + o.values.length; + } + + int ownSize() { + return values.length + this.values.length; + } + + static int firstRow(@Refinement("length(grid) > 0") int[][] grid) { + @Refinement("_ > 0") + int rows = grid.length; + return rows + grid[0].length; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLengthOfArrayExpression.java b/liquidjava-example/src/main/java/testSuite/ErrorLengthOfArrayExpression.java new file mode 100644 index 00000000..49a64b66 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLengthOfArrayExpression.java @@ -0,0 +1,14 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorLengthOfArrayExpression { + + static int nonNegative(@Refinement("_ >= 0") int x) { + return x; + } + + static int rowSize(int[][] grid, int i) { + return nonNegative(grid[i].length - 10); // Expect: Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 995c5927..0161e3e8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -332,9 +332,14 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName))); } else if (fieldRead.getVariable().getSimpleName().equals("length")) { - String targetName = fieldRead.getTarget().toString(); - fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), - BuiltinFunctionPredicate.length(targetName, fieldRead))); + // only a local variable or parameter can be named in a refinement; the length of any other array + // expression (e.g. grid[i], o.arr() or this.arr) is left unconstrained + CtExpression target = fieldRead.getTarget(); + Predicate lengthRefinement = new Predicate(); + if (target instanceof CtVariableRead && !(target instanceof CtFieldRead)) + lengthRefinement = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), + BuiltinFunctionPredicate.length(target.toString(), fieldRead)); + fieldRead.putMetadata(Keys.REFINEMENT, lengthRefinement); } else if (fieldRead.getVariable().getDeclaringType().getDeclaration() instanceof CtEnum) { // only enums declared in the analyzed sources can be translated to SMT String target = fieldRead.getVariable().getDeclaringType().getSimpleName(); From a0b466ae2aa6214f40aba8dad246bc32a82550ee Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 13 Oct 2026 09:56:58 +0100 Subject: [PATCH 2/4] Pack spread varargs arguments into one array argument (#349) Arguments were matched one-to-one with the method parameters, so a call to a varargs method with more arguments than parameters indexed past the parameter list and crashed (`Index 1 out of bounds for length 1`), and a call with zero or one spread argument was checked against the varargs parameter as if that argument were the array itself. When a call passes its trailing arguments individually (the argument count differs from the parameter count, or the last argument is not a subtype of the array type and not null), the varargs parameter is now bound to a fresh array instance whose only refinement is its length (the number of spread arguments). Refinements on the varargs parameter are checked against that array; the individual elements are not checked against anything. Passing an explicit array keeps the one-to-one mapping. Parameter checking now iterates over the mapped parameters instead of the arguments. Fixes #349 Co-Authored-By: Claude Opus 5.5 --- .../java/testSuite/CorrectVarargsCall.java | 35 ++++++++++++ .../java/testSuite/ErrorEmptyVarargsCall.java | 14 +++++ .../main/java/testSuite/ErrorVarargsCall.java | 14 +++++ .../MethodsFunctionsChecker.java | 57 ++++++++++++++++--- 4 files changed, 111 insertions(+), 9 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorEmptyVarargsCall.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorVarargsCall.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java b/liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java new file mode 100644 index 00000000..efe17662 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java @@ -0,0 +1,35 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class CorrectVarargsCall { + + static int count(String... names) { + return names.length; + } + + static int first(@Refinement("length(xs) > 0") int... xs) { + return xs[0]; + } + + static int pick(@Refinement("k >= 0") int k, int... xs) { + return k; + } + + CorrectVarargsCall(@Refinement("length(xs) > 1") int... xs) { + } + + public static void main(String[] args) { + int a = count(); + int b = count("a"); + int c = count("a", "b", "c"); + int d = count(new String[] { "x" }); + int e = count(args); + int f = first(1, 2); + int g = first(5); + int h = pick(0); + int i = pick(1, 2, 3); + int j = count("a", "b") + 1; + new CorrectVarargsCall(1, 2); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEmptyVarargsCall.java b/liquidjava-example/src/main/java/testSuite/ErrorEmptyVarargsCall.java new file mode 100644 index 00000000..ccbeb260 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorEmptyVarargsCall.java @@ -0,0 +1,14 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorEmptyVarargsCall { + + static int first(@Refinement("length(xs) > 0") int... xs) { + return xs[0]; + } + + public static void main(String[] args) { + int a = first(); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorVarargsCall.java b/liquidjava-example/src/main/java/testSuite/ErrorVarargsCall.java new file mode 100644 index 00000000..c07acaf3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorVarargsCall.java @@ -0,0 +1,14 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorVarargsCall { + + static int pick(@Refinement("k >= 0") int k, int... xs) { + return k; + } + + public static void main(String[] args) { + int i = pick(-1, 2, 3); // Expect: Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 6002a408..e1acb01c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -20,10 +20,12 @@ import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Types; +import spoon.reflect.code.CtAbstractInvocation; import spoon.reflect.code.CtConstructorCall; import spoon.reflect.code.CtExpression; import spoon.reflect.code.CtFieldRead; import spoon.reflect.code.CtInvocation; +import spoon.reflect.code.CtLiteral; import spoon.reflect.code.CtReturn; import spoon.reflect.code.CtVariableRead; import spoon.reflect.declaration.CtClass; @@ -332,7 +334,7 @@ private Map checkInvocationRefinements(CtElement invocation, Lis f = rtc.getContext().getFunction(methodName, className, paramTypes); if (f == null) return new HashMap<>(); - Map map = mapInvocation(arguments, f); + Map map = mapInvocation(invocation, arguments, f); String returnViName = prepareReturnInstance(invocation, f); @@ -351,7 +353,7 @@ private Map checkInvocationRefinements(CtElement invocation, Lis return map; } - checkParameters(invocation, arguments, f, map); + checkParameters(invocation, f, map); if (target != null) AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation); @@ -412,10 +414,18 @@ private void applyReturnRefinement(CtElement invocation, RefinedFunction f, Map< invocation.putMetadata(Keys.REFINEMENT, methodRef); } - private Map mapInvocation(List> arguments, RefinedFunction f) { + private Map mapInvocation(CtElement invocation, List> arguments, + RefinedFunction f) { Map mapInvocation = new HashMap<>(); List functionParams = f.getArguments(); - for (int i = 0; i < arguments.size(); i++) { + int mapped = arguments.size(); + if (spreadsVarargs(invocation, arguments, functionParams.size())) { + // the trailing arguments are packed into a new array, which is what the varargs parameter refers to + mapped = functionParams.size() - 1; + Variable varargs = functionParams.get(mapped); + mapInvocation.put(varargs.getName(), createVarargsArray(invocation, varargs, arguments.size() - mapped)); + } + for (int i = 0; i < mapped; i++) { Variable fArg = functionParams.get(i); CtExpression iArg = arguments.get(i); String invStr; @@ -433,6 +443,36 @@ private Map mapInvocation(List> arguments, Refin return mapInvocation; } + /** + * Whether a call to a varargs method passes its trailing arguments individually (zero, one or several of them) + * instead of passing an array as the varargs parameter. + */ + private boolean spreadsVarargs(CtElement invocation, List> arguments, int paramCount) { + if (paramCount == 0 || !(invocation instanceof CtAbstractInvocation inv)) + return false; + CtExecutable method = inv.getExecutable().getExecutableDeclaration(); + if (method == null || method.getParameters().size() != paramCount) + return false; + CtParameter last = method.getParameters().get(paramCount - 1); + if (!last.isVarArgs()) + return false; + if (arguments.size() != paramCount) + return true; + CtExpression lastArg = arguments.get(paramCount - 1); + if (lastArg instanceof CtLiteral lit && lit.getValue() == null) + return false; // a null array + CtTypeReference argType = lastArg.getType(); + return argType == null || !argType.isSubtypeOf(last.getType()); + } + + private String createVarargsArray(CtElement invocation, Variable fArg, int length) { + String nVar = String.format(Formats.INSTANCE, fArg.getName(), rtc.getContext().getCounter()); + Predicate lengthRef = Predicate.createEquals(Predicate.createInvocation("length", Predicate.createVar(nVar)), + Predicate.createLit(String.valueOf(length), Types.INT)); + rtc.getContext().addInstanceToContext(nVar, fArg.getType(), lengthRef, invocation); + return nVar; + } + private String createVariableRepresentingArgument(CtExpression iArg, Variable fArg) { Predicate met = (Predicate) iArg.getMetadata(Keys.REFINEMENT); if (met == null) @@ -444,11 +484,10 @@ private String createVariableRepresentingArgument(CtExpression iArg, Variable return nVar; } - private void checkParameters(CtElement invocation, List> arguments, RefinedFunction f, - Map map) throws LJError { - List functionParams = f.getArguments(); - for (int i = 0; i < arguments.size(); i++) { - Variable fArg = functionParams.get(i); + private void checkParameters(CtElement invocation, RefinedFunction f, Map map) throws LJError { + for (Variable fArg : f.getArguments()) { + if (!map.containsKey(fArg.getName())) + continue; Predicate c = fArg.getMainRefinement(); c = c.substituteVariable(fArg.getName(), map.get(fArg.getName())); List vars = c.getVariableNames(); From 8843527d2d8e54e6640b3ddc9b27b35fb45876ee Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 13 Oct 2026 09:56:58 +0100 Subject: [PATCH 3/4] Add regression tests for type-pattern switches (#345) The `PartialSourcePosition only contains a CompilationUnit` crash came from Spoon 10.4.2 at the old compliance level; it no longer reproduces since Spoon 11.5.0 and compliance level detection (#352, #368). Pattern switches need Java 21, above the level of liquidjava-example (20, where they fail to compile and produce a position-less warning), so the tests verify a temporary project that declares release 21: a pattern switch expression and statement (with a guard and the pattern variable used in the case body) verify cleanly, and a violation inside a pattern case body is still reported. Fixes #345 Co-Authored-By: Claude Opus 5.5 --- .../api/tests/TestPatternSwitch.java | 83 +++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestPatternSwitch.java diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestPatternSwitch.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestPatternSwitch.java new file mode 100644 index 00000000..c7906317 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestPatternSwitch.java @@ -0,0 +1,83 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; + +import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.io.TempDir; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.LJError; + +/** + * Type-pattern switches need Java 21, above the level of liquidjava-example, so they are verified here in a project + * that declares release 21 (#345). + */ +class TestPatternSwitch { + + @TempDir + Path project; + + private Diagnostics verify(String className, String source) throws IOException { + Files.writeString(project.resolve("pom.xml"), + "4.0.021" + + ""); + Path src = Files.createDirectories(project.resolve("src")); + Files.writeString(src.resolve(className + ".java"), source); + CommandLineLauncher.launch(src.toString()); + return Diagnostics.getInstance(); + } + + @Test + void verifiesTypePatternSwitch() throws IOException { + Diagnostics diagnostics = verify("Kinds", """ + public class Kinds { + static String kind(Object o) { + return switch (o) { + case String s -> "string " + s; + case Integer i when i > 0 -> "positive"; + default -> "other"; + }; + } + + static int size(Object o) { + switch (o) { + case String s -> { return s.length(); } + default -> { return 0; } + } + } + } + """); + assertTrue(diagnostics.getErrors().isEmpty(), diagnostics.getErrorOutput()); + assertTrue(diagnostics.getWarnings().isEmpty(), diagnostics.getWarningOutput()); + } + + @Test + void checksRefinementsInsidePatternCase() throws IOException { + Diagnostics diagnostics = verify("Cases", """ + import liquidjava.specification.Refinement; + + public class Cases { + static int positive(@Refinement("_ > 0") int x) { + return x; + } + + static int kind(Object o) { + return switch (o) { + case String s -> positive(-1); + default -> 0; + }; + } + } + """); + assertEquals(1, diagnostics.getErrors().size(), diagnostics.getErrorOutput()); + LJError error = diagnostics.getErrors().iterator().next(); + assertEquals("Refinement Error", error.getTitle()); + assertEquals(10, error.getPosition().getLine()); + } +} From 7f18649e659ea09d6743d8474aacd23040d8b7f1 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 13 Oct 2026 14:08:50 +0100 Subject: [PATCH 4/4] 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 --- .../java/testSuite/CorrectVarargsCall.java | 7 +++++ .../java/testSuite/ErrorVarargsLoopState.java | 27 +++++++++++++++++++ .../RefinementTypeChecker.java | 2 +- .../general_checkers/OperationsChecker.java | 5 ++-- .../src/main/java/liquidjava/utils/Utils.java | 11 ++++++++ 5 files changed, 49 insertions(+), 3 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorVarargsLoopState.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java b/liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java index efe17662..04a786ae 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java +++ b/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); } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorVarargsLoopState.java b/liquidjava-example/src/main/java/testSuite/ErrorVarargsLoopState.java new file mode 100644 index 00000000..33b23faf --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 0161e3e8..b250346b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -677,7 +677,7 @@ private void havocChangedIn(CtLoop loop) { Set 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); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 8e387712..c618ec82 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/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!! diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 018287e4..c3745cfd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/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)