From a523d6f102ead8f14a2551bdbcd7f0ffc2118759 Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Tue, 31 Oct 2017 15:44:58 +0000 Subject: [PATCH] Add a helper function for accessing the element type of a Java array type --- src/java_bytecode/java_types.cpp | 11 +++++++++++ src/java_bytecode/java_types.h | 1 + 2 files changed, 12 insertions(+) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 92b2ab27dcb..3f61e14ccba 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -123,6 +123,17 @@ 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) +{ + 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/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index a51a6c3db95..740d347feb7 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -56,6 +56,7 @@ 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); bool is_reference_type(char t);