|
const annotated_typet & | to_annotated_type (const typet &type) |
|
annotated_typet & | to_annotated_type (typet &type) |
|
template<> |
bool | can_cast_type< annotated_typet > (const typet &) |
|
template<> |
bool | can_cast_type< java_method_typet > (const typet &type) |
|
const java_method_typet & | to_java_method_type (const typet &type) |
|
java_method_typet & | to_java_method_type (typet &type) |
|
const java_class_typet & | to_java_class_type (const typet &type) |
|
java_class_typet & | to_java_class_type (typet &type) |
|
template<> |
bool | can_cast_type< java_class_typet > (const typet &type) |
|
template<> |
bool | can_cast_type< java_reference_typet > (const typet &type) |
|
const java_reference_typet & | to_java_reference_type (const typet &type) |
|
java_reference_typet & | to_java_reference_type (typet &type) |
|
signedbv_typet | java_int_type () |
|
signedbv_typet | java_long_type () |
|
signedbv_typet | java_short_type () |
|
signedbv_typet | java_byte_type () |
|
unsignedbv_typet | java_char_type () |
|
floatbv_typet | java_float_type () |
|
floatbv_typet | java_double_type () |
|
c_bool_typet | java_boolean_type () |
|
empty_typet | java_void_type () |
|
java_reference_typet | java_reference_type (const struct_tag_typet &subtype) |
|
reference_typet | java_reference_type (const typet &subtype) |
|
java_reference_typet | java_lang_object_type () |
|
struct_tag_typet | java_classname (const std::string &) |
|
java_reference_typet | java_array_type (const char subtype) |
| Construct an array pointer type.
|
|
java_reference_typet | java_reference_array_type (const struct_tag_typet &element_type) |
|
const typet & | java_array_element_type (const struct_tag_typet &array_symbol) |
| Return a const reference to the element type of a given java array type.
|
|
typet & | java_array_element_type (struct_tag_typet &array_symbol) |
| Return a non-const reference to the element type of a given java array type.
|
|
bool | is_java_array_type (const typet &type) |
| Checks whether the given type is an array pointer type.
|
|
bool | is_multidim_java_array_type (const typet &type) |
| 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.
|
|
std::pair< typet, std::size_t > | java_array_dimension_and_element_type (const struct_tag_typet &type) |
| Returns the underlying element type and array dimensionality of Java struct type .
|
|
exprt | get_array_dimension_field (const exprt &pointer) |
|
exprt | get_array_element_type_field (const exprt &pointer) |
|
typet | java_type_from_char (char t) |
| Constructs a type indicated by the given character:
|
|
std::optional< typet > | java_type_from_string (const std::string &, const std::string &class_name_prefix="") |
| Transforms a string representation of a Java type into an internal type representation thereof.
|
|
char | java_char_from_type (const typet &type) |
|
std::vector< typet > | java_generic_type_from_string (const std::string &, const std::string &) |
| Converts the content of a generic class type into a vector of Java types, that is each type variable of the class has one entry in the returned vector.
|
|
typet | java_bytecode_promotion (const typet &) |
| Java does not support byte/short return types. These are always promoted.
|
|
exprt | java_bytecode_promotion (const exprt &) |
| Java does not support byte/short return types. These are always promoted.
|
|
size_t | find_closing_semi_colon_for_reference_type (const std::string src, size_t starting_point=0) |
| Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point .
|
|
std::vector< std::string > | parse_raw_list_types (std::string src, char opening_bracket, char closing_bracket) |
| Given a substring of a descriptor or signature that contains one or more types parse out the individual type strings.
|
|
bool | is_java_array_tag (const irep_idt &tag) |
| See above.
|
|
bool | is_valid_java_array (const struct_typet &) |
| Programmatic documentation of the structure of a Java array (of either primitives or references) type.
|
|
bool | equal_java_types (const typet &type1, const typet &type2) |
| Compares the types, including checking element types if both types are arrays.
|
|
bool | is_java_generic_parameter_tag (const typet &type) |
| Checks whether the type is a java generic parameter/variable, e.g., T in List<T> .
|
|
const java_generic_parameter_tagt & | to_java_generic_parameter_tag (const typet &type) |
|
java_generic_parameter_tagt & | to_java_generic_parameter_tag (typet &type) |
|
template<> |
bool | can_cast_type< java_generic_parametert > (const typet &base) |
| Check whether a reference to a typet is a Java generic parameter/variable, e.g., T in List<T> .
|
|
bool | is_java_generic_parameter (const typet &type) |
| Checks whether the type is a java generic parameter/variable, e.g., T in List<T> .
|
|
const java_generic_parametert & | to_java_generic_parameter (const typet &type) |
|
java_generic_parametert & | to_java_generic_parameter (typet &type) |
|
bool | is_java_generic_struct_tag_type (const typet &type) |
|
const java_generic_struct_tag_typet & | to_java_generic_struct_tag_type (const typet &type) |
|
java_generic_struct_tag_typet & | to_java_generic_struct_tag_type (typet &type) |
|
template<> |
bool | can_cast_type< java_generic_typet > (const typet &type) |
|
bool | is_java_generic_type (const typet &type) |
|
const java_generic_typet & | to_java_generic_type (const typet &type) |
|
java_generic_typet & | to_java_generic_type (typet &type) |
|
bool | is_java_generic_class_type (const typet &type) |
|
const java_generic_class_typet & | to_java_generic_class_type (const java_class_typet &type) |
|
java_generic_class_typet & | to_java_generic_class_type (java_class_typet &type) |
|
const typet & | java_generic_get_inst_type (size_t index, const java_generic_typet &type) |
| Access information of type arguments of java instantiated type.
|
|
const irep_idt & | java_generic_class_type_var (size_t index, const java_generic_class_typet &type) |
| Access information of type variables of a generic java class type.
|
|
const typet & | java_generic_class_type_bound (size_t index, const typet &t) |
| Access information of the type bound of a generic java class type.
|
|
bool | is_java_implicitly_generic_class_type (const typet &type) |
|
const java_implicitly_generic_class_typet & | to_java_implicitly_generic_class_type (const java_class_typet &type) |
|
java_implicitly_generic_class_typet & | to_java_implicitly_generic_class_type (java_class_typet &type) |
|
std::vector< java_generic_parametert > | get_all_generic_parameters (const typet &type) |
|
std::optional< typet > | java_type_from_string_with_exception (const std::string &descriptor, const std::optional< std::string > &signature, const std::string &class_name) |
|
const std::optional< size_t > | java_generics_get_index_for_subtype (const std::vector< java_generic_parametert > &gen_types, const irep_idt &identifier) |
| Get the index in the subtypes array for a given component.
|
|
void | get_dependencies_from_generic_parameters (const std::string &, std::set< irep_idt > &) |
| Collect information about generic type parameters from a given signature.
|
|
void | get_dependencies_from_generic_parameters (const typet &, std::set< irep_idt > &) |
| Collect information about generic type parameters from a given type.
|
|
std::string | erase_type_arguments (const std::string &) |
| Take a signature string and remove everything in angle brackets allowing for the type to be parsed normally, for example java.util.HashSet<java.lang.Integer> will be turned into java.util.HashSet
|
|
std::string | gather_full_class_name (const std::string &) |
| Returns the full class name, skipping over the generics.
|
|
std::string | pretty_java_type (const typet &) |
|
std::string | pretty_signature (const java_method_typet &) |
|