NathanJPhillips
diff --git a/‎jbmc/unit/java_bytecode/java_bytecode_parser/CustomException.class‎
0 Bytes b/‎jbmc/unit/java_bytecode/java_bytecode_parser/CustomException.class‎
0 Bytes
diff --git a/‎jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.class‎
72 Bytes b/‎jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.class‎
72 Bytes
diff --git a/‎jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java‎
Lines changed: 4 additions & 0 deletions b/‎jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java‎
Lines changed: 4 additions & 0 deletions
diff --git a/‎jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp‎
Lines changed: 11 additions & 18 deletions b/‎jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp‎
Lines changed: 11 additions & 18 deletions
@@ -8,6 +8,10 @@ public static void test() throws CustomException, IOException {
      throw new CustomException();
   }
 
+  public static void testNoExceptions() {
+    StringReader sr = new StringReader("");
+  }
+
 }
 
 class CustomException extends Exception {
 
@@ -606,8 +606,6 @@ SCENARIO(
     {
       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 java_method_typet method =
@@ -626,23 +624,18 @@ SCENARIO(
             irept("java.io.IOException").id()) != 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")
+    WHEN(
+      "Parsing the exceptions attribute for a method that throws no exceptions")
     {
-      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);
-    }
+      THEN("We should be able to get the list of exceptions it throws")
+      {
+        const symbolt &method_symbol = new_symbol_table.lookup_ref(
+          "java::ThrowsExceptions.testNoExceptions:()V");
+        const java_method_typet method =
+          to_java_method_type(method_symbol.type);
+        const std::vector<irep_idt> exceptions = method.throws_exceptions();
+        REQUIRE(exceptions.size() == 0);
+      }
     }
   }
 }
Original file line number	Diff line number	Diff line change
`@@ -8,6 +8,10 @@ public static void test() throws CustomException, IOException {`
`8`	`8`	`throw new CustomException();`
`9`	`9`	`}`
`10`	`10`
	`11`	`+ public static void testNoExceptions() {`
	`12`	`+ StringReader sr = new StringReader("");`
	`13`	`+ }`
	`14`	`+`
`11`	`15`	`}`
`12`	`16`
`13`	`17`	`class CustomException extends Exception {`
Original file line number	Diff line number	Diff line change
`@@ -606,8 +606,6 @@ SCENARIO(`
`606`	`606`	`{`
`607`	`607`	`THEN("We should be able to get the list of exceptions it throws")`
`608`	`608`	`{`
`609`		`- const symbolt &class_symbol =`
`610`		`- new_symbol_table.lookup_ref("java::ThrowsExceptions");`
`611`	`609`	`const symbolt &method_symbol =`
`612`	`610`	`new_symbol_table.lookup_ref("java::ThrowsExceptions.test:()V");`
`613`	`611`	`const java_method_typet method =`
`@@ -626,23 +624,18 @@ SCENARIO(`
`626`	`624`	`irept("java.io.IOException").id()) != exceptions.end());`
`627`	`625`	`}`
`628`	`626`	`}`
`629`		`- }`
`630`		`-`
`631`		`- const symbol_tablet &new_symbol_table2 = load_java_class(`
`632`		`- "ThrowsExceptions", "./java_bytecode/java_bytecode_parser");`
`633`		`- WHEN(`
`634`		`- "Parsing the exceptions attribute for a method that throws no exceptions")`
`635`		`- {`
`636`		`- THEN("We should be able to get the list of exceptions it throws")`
	`627`	`+ WHEN(`
	`628`	`+ "Parsing the exceptions attribute for a method that throws no exceptions")`
`637`	`629`	`{`
`638`		`- const symbolt &class_symbol =`
`639`		`- new_symbol_table2.lookup_ref("java::ThrowsExceptions");`
`640`		`- const symbolt &method_symbol =`
`641`		`- new_symbol_table2.lookup_ref("java::ThrowsExceptions.test:()V");`
`642`		`- const java_method_typet method = to_java_method_type(method_symbol.type);`
`643`		`- const std::vector<irept> exceptions = method.throws_exceptions();`
`644`		`- REQUIRE(exceptions.size() == 0);`
`645`		`- }`
	`630`	`+ THEN("We should be able to get the list of exceptions it throws")`
	`631`	`+ {`
	`632`	`+ const symbolt &method_symbol = new_symbol_table.lookup_ref(`
	`633`	`+ "java::ThrowsExceptions.testNoExceptions:()V");`
	`634`	`+ const java_method_typet method =`
	`635`	`+ to_java_method_type(method_symbol.type);`
	`636`	`+ const std::vector<irep_idt> exceptions = method.throws_exceptions();`
	`637`	`+ REQUIRE(exceptions.size() == 0);`
	`638`	`+ }`
`646`	`639`	`}`
`647`	`640`	`}`
`648`	`641`	`}`