Parent synthetic classes should preserve method exceptions

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<String> throwsList;
+
   /**
    * Create an instance of UnsolvedMethod
    *
@@ -78,11 +81,39 @@ public UnsolvedMethod(
       List<String> 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<String> parameterList,
+      boolean isJustMethodSignature,
+      String accessModifier,
+      List<String> 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 {

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<String> listOfParameters = new ArrayList<>();
+    List<String> 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);

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()"});
+  }
+}

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

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

src/test/resources/inheritmethodexception/expected/com/example/UnknownException.java

@@ -0,0 +1,4 @@
+package com.example;
+
+public class UnknownException extends java.lang.Throwable {
+}

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