Add functions to retrieve a reference to the java array element type

NathanJPhillips · Jul 17, 2018 · f10badb · f10badb
1 parent a18b32d
commit f10badb
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 8 deletions.
diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp
@@ -120,15 +120,24 @@ reference_typet java_array_type(const char subtype)
   return java_reference_type(symbol_type);
 }
 
-/// Return the type of the elements of a given java array type
-/// \param array_type The java array type
-/// \return The type of the elements of the array
-typet java_array_element_type(const symbol_typet &array_type)
+/// Return a const reference to the element type of a given java array type
+/// \param array_symbol The java array type
+const typet &java_array_element_type(const symbol_typet &array_symbol)
 {
-  INVARIANT(
-    is_java_array_tag(array_type.get_identifier()),
+  DATA_INVARIANT(
+    is_java_array_tag(array_symbol.get_identifier()),
+    "Symbol should have array tag");
+  return array_symbol.find_type(ID_C_element_type);
+}
+
+/// Return a non-const reference to the element type of a given java array type
+/// \param array_symbol The java array type
+typet &java_array_element_type(symbol_typet &array_symbol)
+{
+  DATA_INVARIANT(
+    is_java_array_tag(array_symbol.get_identifier()),
     "Symbol should have array tag");
-  return array_type.find_type(ID_C_element_type);
+  return array_symbol.add_type(ID_C_element_type);
 }
 
 /// See above

diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
@@ -245,7 +245,8 @@ reference_typet java_lang_object_type();
 symbol_typet java_classname(const std::string &);
 
 reference_typet java_array_type(const char subtype);
-typet java_array_element_type(const symbol_typet &array_type);
+const typet &java_array_element_type(const symbol_typet &array_symbol);
+typet &java_array_element_type(symbol_typet &array_symbol);
 
 bool is_reference_type(char t);