Add a check functions for (multi-dimensional) array types

svorenova · svorenova · commit e66f76f5a2d8 · 2018-07-25T15:28:12.000+01:00
diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp
@@ -140,6 +140,25 @@ typet &java_array_element_type(symbol_typet &array_symbol)
   return array_symbol.add_type(ID_C_element_type);
 }
 
+/// Checks whether the given type is an array pointer type
+bool is_java_array_type(const typet &type)
+{
+  if(!(type.id() == ID_pointer && type.subtype().id() == ID_symbol))
+    return false;
+  const auto &subtype_symbol = to_symbol_type(type.subtype());
+  return is_java_array_tag(subtype_symbol.get_identifier());
+}
+
+/// Checks whether the given type is a multi-dimensional array pointer type,
+// i.e., a pointer to an array type with element type also being a pointer to an
+/// array type.
+bool is_multidim_java_array_type(const typet &type)
+{
+  return is_java_array_type(type) &&
+         is_java_array_type(
+           java_array_element_type(to_symbol_type(type.subtype())));
+}
+
 /// 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
@@ -247,6 +247,8 @@ symbol_typet java_classname(const std::string &);
 reference_typet java_array_type(const char subtype);
 const typet &java_array_element_type(const symbol_typet &array_symbol);
 typet &java_array_element_type(symbol_typet &array_symbol);
+bool is_java_array_type(const typet &type);
+bool is_multidim_java_array_type(const typet &type);
 
 bool is_reference_type(char t);
 
