diff --git a/src/main/java/org/checkerframework/specimin/TargetMethodFinderVisitor.java b/src/main/java/org/checkerframework/specimin/TargetMethodFinderVisitor.java index e02a577a..34e8a9e6 100644 --- a/src/main/java/org/checkerframework/specimin/TargetMethodFinderVisitor.java +++ b/src/main/java/org/checkerframework/specimin/TargetMethodFinderVisitor.java @@ -12,13 +12,13 @@ import com.github.javaparser.ast.expr.ObjectCreationExpr; import com.github.javaparser.ast.expr.SuperExpr; import com.github.javaparser.ast.stmt.ExplicitConstructorInvocationStmt; -import com.github.javaparser.ast.type.ReferenceType; import com.github.javaparser.ast.type.Type; import com.github.javaparser.ast.visitor.ModifierVisitor; import com.github.javaparser.ast.visitor.Visitable; import com.github.javaparser.resolution.declarations.ResolvedConstructorDeclaration; import com.github.javaparser.resolution.declarations.ResolvedFieldDeclaration; import com.github.javaparser.resolution.declarations.ResolvedValueDeclaration; +import com.github.javaparser.resolution.types.ResolvedReferenceType; import java.util.ArrayList; import java.util.HashSet; import java.util.List; @@ -195,7 +195,9 @@ public Visitable visit(MethodDeclaration method, Void p) { targetMethods.add(method.resolve().getQualifiedSignature()); unfoundMethods.remove(methodName); Type returnType = method.getType(); - if (returnType instanceof ReferenceType) { + // JavaParser may misinterpret unresolved array types as reference types. + // To ensure accuracy, we resolve the type before proceeding with the check. + if (returnType.resolve() instanceof ResolvedReferenceType) { usedClass.add(returnType.resolve().asReferenceType().getQualifiedName()); } } diff --git a/src/test/java/org/checkerframework/specimin/ArrayTypeTest.java b/src/test/java/org/checkerframework/specimin/ArrayTypeTest.java new file mode 100644 index 00000000..bea6d3e4 --- /dev/null +++ b/src/test/java/org/checkerframework/specimin/ArrayTypeTest.java @@ -0,0 +1,17 @@ +package org.checkerframework.specimin; + +import java.io.IOException; +import org.junit.Test; + +/** + * This test checks if Specimin will work for array types + */ +public class ArrayTypeTest { + @Test + public void runTest() throws IOException { + SpeciminTestExecutor.runTestWithoutJarPaths( + "arrayType", + new String[] {"com/example/Simple.java"}, + new String[] {"com.example.Simple#sortArray(int[])"}); + } +} diff --git a/src/test/resources/arrayType/expected/com/example/Simple.java b/src/test/resources/arrayType/expected/com/example/Simple.java new file mode 100644 index 00000000..258a473e --- /dev/null +++ b/src/test/resources/arrayType/expected/com/example/Simple.java @@ -0,0 +1,11 @@ +package com.example; + +import java.util.Arrays; + +class Simple { + + public static int[] sortArray(int[] array) { + Arrays.sort(array); + return array; + } +} diff --git a/src/test/resources/arrayType/input/com/example/Simple.java b/src/test/resources/arrayType/input/com/example/Simple.java new file mode 100644 index 00000000..bbd4e911 --- /dev/null +++ b/src/test/resources/arrayType/input/com/example/Simple.java @@ -0,0 +1,11 @@ +package com.example; + +import java.util.Arrays; + +class Simple { + // Target method. + public static int[] sortArray(int[] array) { + Arrays.sort(array); + return array; + } +}