diff --git a/src/main/java/org/checkerframework/specimin/UnsolvedMethod.java b/src/main/java/org/checkerframework/specimin/UnsolvedMethod.java index 6c187a83f..048b6f3ff 100644 --- a/src/main/java/org/checkerframework/specimin/UnsolvedMethod.java +++ b/src/main/java/org/checkerframework/specimin/UnsolvedMethod.java @@ -37,6 +37,9 @@ public class UnsolvedMethod { /** Access modifer of the current method. The value is set to "public" by default. */ private final String accessModifier; + /** The list of the types of the exceptions thrown by the method. */ + private final List throwsList; + /** * Create an instance of UnsolvedMethod * @@ -78,11 +81,39 @@ public UnsolvedMethod( List parameterList, boolean isJustMethodSignature, String accessModifier) { + this( + name, + returnType, + parameterList, + isJustMethodSignature, + accessModifier, + Collections.emptyList()); + } + + /** + * Create an instance of UnsolvedMethod for a synthetic interface. + * + * @param name the name of the method + * @param returnType the return type of the method + * @param parameterList the list of parameters for this method + * @param isJustMethodSignature indicates whether this method represents just a method signature + * without a body + * @param accessModifier the access modifier of the current method + * @param throwsList the list of exceptions thrown by this method + */ + public UnsolvedMethod( + String name, + String returnType, + List parameterList, + boolean isJustMethodSignature, + String accessModifier, + List throwsList) { this.name = name; this.returnType = returnType; this.parameterList = parameterList; this.isJustMethodSignature = isJustMethodSignature; this.accessModifier = accessModifier; + this.throwsList = throwsList; } /** @@ -172,6 +203,21 @@ public String toString() { signature.append(name).append("("); signature.append(arguments); signature.append(")"); + + if (throwsList.size() > 0) { + signature.append(" throws "); + } + + StringBuilder exceptions = new StringBuilder(); + for (int i = 0; i < throwsList.size(); i++) { + String exception = throwsList.get(i); + exceptions.append(exception); + if (i < parameterList.size() - 1) { + arguments.append(", "); + } + } + signature.append(exceptions); + if (isJustMethodSignature) { return signature.append(";").toString(); } else { diff --git a/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java b/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java index 3018eb6fb..c829082ea 100644 --- a/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java +++ b/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java @@ -1847,6 +1847,7 @@ public void updateUnsolvedClassOrInterfaceWithMethod( Node method, String className, String desiredReturnType, boolean updatingInterface) { String methodName = ""; List listOfParameters = new ArrayList<>(); + List listOfExceptions = new ArrayList<>(); String accessModifer = "public"; if (method instanceof MethodCallExpr) { methodName = ((MethodCallExpr) method).getNameAsString(); @@ -1855,9 +1856,11 @@ public void updateUnsolvedClassOrInterfaceWithMethod( } // method is a MethodDeclaration else { - methodName = ((MethodDeclaration) method).getNameAsString(); - accessModifer = ((MethodDeclaration) method).getAccessSpecifier().asString(); - for (Parameter para : ((MethodDeclaration) method).getParameters()) { + MethodDeclaration methodDecl = (MethodDeclaration) method; + + methodName = methodDecl.getNameAsString(); + accessModifer = methodDecl.getAccessSpecifier().asString(); + for (Parameter para : methodDecl.getParameters()) { Type paraType = para.getType(); String paraTypeAsString = paraType.asString(); try { @@ -1870,6 +1873,19 @@ public void updateUnsolvedClassOrInterfaceWithMethod( } listOfParameters.add(paraTypeAsString); } + + for (ReferenceType exception : methodDecl.getThrownExceptions()) { + String exceptionTypeAsString = exception.asString(); + try { + // if possible, opt for fully-qualified names. + exceptionTypeAsString = exception.resolve().describe(); + } catch (UnsolvedSymbolException | UnsupportedOperationException e) { + // avoiding ignored catch blocks errors. + listOfExceptions.add(exceptionTypeAsString); + continue; + } + listOfExceptions.add(exceptionTypeAsString); + } } String returnType = ""; if (desiredReturnType.equals("")) { @@ -1879,7 +1895,12 @@ public void updateUnsolvedClassOrInterfaceWithMethod( } UnsolvedMethod thisMethod = new UnsolvedMethod( - methodName, returnType, listOfParameters, updatingInterface, accessModifer); + methodName, + returnType, + listOfParameters, + updatingInterface, + accessModifer, + listOfExceptions); UnsolvedClassOrInterface missingClass = updateUnsolvedClassWithClassName(className, false, false, thisMethod); syntheticMethodReturnTypeAndClass.put(returnType, missingClass); diff --git a/src/test/java/org/checkerframework/specimin/InheritMethodExceptionTest.java b/src/test/java/org/checkerframework/specimin/InheritMethodExceptionTest.java new file mode 100644 index 000000000..7daf22959 --- /dev/null +++ b/src/test/java/org/checkerframework/specimin/InheritMethodExceptionTest.java @@ -0,0 +1,18 @@ +package org.checkerframework.specimin; + +import java.io.IOException; +import org.junit.Test; + +/** + * This test checks that, given an @Override method with a throws clause in a child class, Specimin + * will preserve the exceptions in its synthetic parent definition + */ +public class InheritMethodExceptionTest { + @Test + public void runTest() throws IOException { + SpeciminTestExecutor.runTestWithoutJarPaths( + "inheritmethodexception", + new String[] {"com/example/Simple.java"}, + new String[] {"com.example.Simple#foo()"}); + } +} diff --git a/src/test/resources/inheritmethodexception/expected/com/example/Parent.java b/src/test/resources/inheritmethodexception/expected/com/example/Parent.java new file mode 100644 index 000000000..28d9c6c35 --- /dev/null +++ b/src/test/resources/inheritmethodexception/expected/com/example/Parent.java @@ -0,0 +1,8 @@ +package com.example; + +public class Parent { + + public void foo() throws UnknownException { + throw new Error(); + } +} diff --git a/src/test/resources/inheritmethodexception/expected/com/example/Simple.java b/src/test/resources/inheritmethodexception/expected/com/example/Simple.java new file mode 100644 index 000000000..0a092040a --- /dev/null +++ b/src/test/resources/inheritmethodexception/expected/com/example/Simple.java @@ -0,0 +1,8 @@ +package com.example; + +public class Simple extends Parent { + + public void foo() throws UnknownException { + throw new Exception(); + } +} diff --git a/src/test/resources/inheritmethodexception/expected/com/example/UnknownException.java b/src/test/resources/inheritmethodexception/expected/com/example/UnknownException.java new file mode 100644 index 000000000..c3b118463 --- /dev/null +++ b/src/test/resources/inheritmethodexception/expected/com/example/UnknownException.java @@ -0,0 +1,4 @@ +package com.example; + +public class UnknownException extends java.lang.Throwable { +} diff --git a/src/test/resources/inheritmethodexception/input/com/example/Simple.java b/src/test/resources/inheritmethodexception/input/com/example/Simple.java new file mode 100644 index 000000000..4752d42da --- /dev/null +++ b/src/test/resources/inheritmethodexception/input/com/example/Simple.java @@ -0,0 +1,8 @@ +package com.example; + +public class Simple extends Parent { + @Override + public void foo() throws UnknownException { + throw new Exception(); + } +} \ No newline at end of file