Refactors interface for exceptions to not use irepts.

Author: jeannielynnmoulton

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);
 

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

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp

@@ -612,17 +612,18 @@ SCENARIO(
           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());
       }
     }
   }