Add function to retrieve a reference to the element type of a java array

diffblue · Jul 4, 2018 · 9b8cfc2 · 9b8cfc2
1 parent 6e554d9
commit 9b8cfc2
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp
@@ -131,6 +131,17 @@ typet java_array_element_type(const symbol_typet &array_type)
   return array_type.find_type(ID_C_element_type);
 }
 
+/// Return a const reference to the element type of a given java array type
+/// \param array_type The java array type
+const typet &java_array_element_type_ref(const symbol_typet &array_type)
+{
+  INVARIANT(
+    is_java_array_tag(array_type.get_identifier()),
+    "Symbol should have array tag");
+  return array_type.find_type(ID_C_element_type);
+}
+
+
 /// See above
 /// \par parameters: Struct tag 'tag'
 /// \return True if the given struct is a Java array

diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
@@ -206,6 +206,7 @@ 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_ref(const symbol_typet &array_type);
 
 bool is_reference_type(char t);