Unit tests throws exceptions parsing.

Author: jeannielynnmoulton

jbmc/unit/java_bytecode/java_bytecode_parser/CustomException.class

@@ -0,0 +1,14 @@
+import java.io.*;
+
+public class ThrowsExceptions {
+
+  public static void test() throws CustomException, IOException {
+     StringReader sr = new StringReader("");
+     sr.read();
+     throw new CustomException();
+  }
+
+}
+
+class CustomException extends Exception {
+}

jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.class

@@ -8,6 +8,7 @@
 
 #include <java-testing-utils/load_java_class.h>
 #include <java_bytecode/java_bytecode_convert_class.h>
+#include <java_bytecode/java_bytecode_convert_method.h>
 #include <java_bytecode/java_bytecode_parse_tree.h>
 #include <java_bytecode/java_types.h>
 #include <testing-utils/catch.hpp>
@@ -596,4 +597,50 @@ SCENARIO(
       }
     }
   }
+
+  GIVEN("A method that may or may not throw exceptions")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "ThrowsExceptions", "./java_bytecode/java_bytecode_parser");
+    WHEN("Parsing the exceptions attribute for a method that throws exceptions")
+    {
+      THEN("We should be able to get the list of exceptions it throws")
+      {
+        const symbolt &class_symbol =
+          new_symbol_table.lookup_ref("java::ThrowsExceptions");
+        const symbolt &method_symbol =
+          new_symbol_table.lookup_ref("java::ThrowsExceptions.test:()V");
+        const code_typet method = to_code_type(method_symbol.type);
+        const std::vector<irept> exceptions = method.throws_exceptions();
+        REQUIRE(exceptions.size() == 2);
+        REQUIRE(
+          std::find(
+            exceptions.begin(), exceptions.end(), irept("CustomException")) !=
+          exceptions.end());
+        REQUIRE(
+          std::find(
+            exceptions.begin(),
+            exceptions.end(),
+            irept("java.io.IOException")) != exceptions.end());
+      }
+    }
+  }
+
+  const symbol_tablet &new_symbol_table2 = load_java_class(
+      "ThrowsExceptions", "./java_bytecode/java_bytecode_parser");
+  WHEN(
+    "Parsing the exceptions attribute for a method that throws no exceptions")
+  {
+    THEN("We should be able to get the list of exceptions it throws")
+    {
+      const symbolt &class_symbol =
+        new_symbol_table2.lookup_ref("java::ThrowsExceptions");
+      const symbolt &method_symbol =
+        new_symbol_table2.lookup_ref("java::ThrowsExceptions.test:()V");
+      const java_method_typet method = to_java_method_type(method_symbol.type);
+      const std::vector<irept> exceptions = method.throws_exceptions();
+      REQUIRE(exceptions.size() == 0);
+    }
+    }
+  }
 }