Refactors interface for exceptions to not use irepts.

jeannielynnmoulton · jeannielynnmoulton · commit 66ba3db5b9bd · 2018-07-31T11:13:30.000+01:00
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -587,9 +587,8 @@ void java_bytecode_convert_methodt::convert(
   method_symbol.location=m.source_location;
   method_symbol.location.set_function(method_identifier);
 
-  std::vector<irept> &exceptions_list = method_type.throws_exceptions();
   for(const auto &exception_name : m.throws_exception_table)
-    exceptions_list.push_back(irept(exception_name));
+    method_type.add_throws_exceptions(exception_name);
 
   const std::string signature_string = pretty_signature(method_type);
 
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
@@ -245,14 +245,17 @@ inline bool can_cast_type<java_class_typet>(const typet &type)
 class java_method_typet : public code_typet
 {
 public:
-  const std::vector<irept> &throws_exceptions() const
+  const std::vector<irep_idt> throws_exceptions() const
   {
-    return find(ID_exceptions_thrown_list).get_sub();
+    std::vector<irep_idt> exceptions;
+    for(const auto &e : find(ID_exceptions_thrown_list).get_sub())
+      exceptions.push_back(e.id());
+    return exceptions;
   }
 
-  std::vector<irept> &throws_exceptions()
+  void add_throws_exceptions(irep_idt exception)
   {
-    return add(ID_exceptions_thrown_list).get_sub();
+    add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
   }
 };
 
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/CustomException.class b/jbmc/unit/java_bytecode/java_bytecode_parser/CustomException.class
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.class
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java b/jbmc/unit/java_bytecode/java_bytecode_parser/ThrowsExceptions.java
@@ -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 {
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp
@@ -606,42 +606,36 @@ 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 =
           to_java_method_type(method_symbol.type);
-        const std::vector<irept> exceptions = method.throws_exceptions();
+        const std::vector<irep_idt> exceptions = method.throws_exceptions();
         REQUIRE(exceptions.size() == 2);
         REQUIRE(
           std::find(
-            exceptions.begin(), exceptions.end(), irept("CustomException")) !=
-          exceptions.end());
+            exceptions.begin(),
+            exceptions.end(),
+            irept("CustomException").id()) != exceptions.end());
         REQUIRE(
           std::find(
             exceptions.begin(),
             exceptions.end(),
-            irept("java.io.IOException")) != exceptions.end());
+            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
`@@ -245,14 +245,17 @@ inline bool can_cast_type<java_class_typet>(const typet &type)`
`245`	`245`	`class java_method_typet : public code_typet`
`246`	`246`	`{`
`247`	`247`	`public:`
`248`		`- const std::vector<irept> &throws_exceptions() const`
	`248`	`+ const std::vector<irep_idt> throws_exceptions() const`
`249`	`249`	`{`
`250`		`- return find(ID_exceptions_thrown_list).get_sub();`
	`250`	`+ std::vector<irep_idt> exceptions;`
	`251`	`+ for(const auto &e : find(ID_exceptions_thrown_list).get_sub())`
	`252`	`+ exceptions.push_back(e.id());`
	`253`	`+ return exceptions;`
`251`	`254`	`}`
`252`	`255`
`253`		`- std::vector<irept> &throws_exceptions()`
	`256`	`+ void add_throws_exceptions(irep_idt exception)`
`254`	`257`	`{`
`255`		`- return add(ID_exceptions_thrown_list).get_sub();`
	`258`	`+ add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));`
`256`	`259`	`}`
`257`	`260`	`};`
`258`	`261`
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 {`