|
CBMC
|
#include <util/invariant.h>#include <algorithm>#include <set>#include <util/c_types.h>#include <util/narrow.h>#include <util/optional.h>#include <util/std_expr.h>
Include dependency graph for java_types.h:
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | java_annotationt |
| class | java_annotationt::valuet |
| class | annotated_typet |
| class | java_method_typet |
| class | java_class_typet |
| class | java_class_typet::componentt |
| class | java_class_typet::methodt |
| class | java_class_typet::java_lambda_method_handlet |
| Represents a lambda call to a method. More... | |
| class | java_reference_typet |
| This is a specialization of reference_typet. More... | |
| class | java_generic_parameter_tagt |
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>. More... | |
| class | java_generic_parametert |
| Reference that points to a java_generic_parameter_tagt. More... | |
| class | java_generic_struct_tag_typet |
Class to hold type with generic type arguments, for example java.util.List in either a reference of type List<Integer> or List<T> (here T must have been concretized already to create this object so technically it is an argument rather than parameter/variable, but in the symbol table this still shows as the parameter T). More... | |
| class | java_generic_typet |
| Reference that points to a java_generic_struct_tag_typet. More... | |
| class | java_generic_class_typet |
| Class to hold a class with generics, extends the java class type with a vector of java generic type parameters (also called type variables). More... | |
| class | java_implicitly_generic_class_typet |
| Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class or a derived class of a generic base class. More... | |
| class | unsupported_java_class_signature_exceptiont |
| An exception that is raised for unsupported class signature. More... | |
Macros | |
| #define | JAVA_REFERENCE_ARRAY_CLASSID "java::array[reference]" |
| #define | JAVA_ARRAY_DIMENSION_FIELD_NAME "@array_dimensions" |
| #define | JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME "@element_class_identifier" |
Functions | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| bool | is_java_array_type (const typet &type) |
| Checks whether the given type is an array pointer type. More... | |
| 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. More... | |
| 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. More... | |
| 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: More... | |
| optionalt< 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. More... | |
| 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. More... | |
| typet | java_bytecode_promotion (const typet &) |
| Java does not support byte/short return types. These are always promoted. More... | |
| exprt | java_bytecode_promotion (const exprt &) |
| Java does not support byte/short return types. These are always promoted. More... | |
| 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. More... | |
| 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. More... | |
| bool | is_java_array_tag (const irep_idt &tag) |
| See above. More... | |
| bool | is_valid_java_array (const struct_typet &) |
| Programmatic documentation of the structure of a Java array (of either primitives or references) type. More... | |
| bool | equal_java_types (const typet &type1, const typet &type2) |
| Compares the types, including checking element types if both types are arrays. More... | |
| 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>. More... | |
| 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>. More... | |
| bool | is_java_generic_parameter (const typet &type) |
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| 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) |
| optionalt< typet > | java_type_from_string_with_exception (const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name) |
| const optionalt< 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. More... | |
| void | get_dependencies_from_generic_parameters (const std::string &, std::set< irep_idt > &) |
| Collect information about generic type parameters from a given signature. More... | |
| void | get_dependencies_from_generic_parameters (const typet &, std::set< irep_idt > &) |
| Collect information about generic type parameters from a given type. More... | |
| 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 More... | |
| std::string | gather_full_class_name (const std::string &) |
| Returns the full class name, skipping over the generics. More... | |
| std::string | pretty_java_type (const typet &) |
| std::string | pretty_signature (const java_method_typet &) |
| #define JAVA_ARRAY_DIMENSION_FIELD_NAME "@array_dimensions" |
Definition at line 669 of file java_types.h.
| #define JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME "@element_class_identifier" |
Definition at line 671 of file java_types.h.
| #define JAVA_REFERENCE_ARRAY_CLASSID "java::array[reference]" |
Definition at line 656 of file java_types.h.
|
inline |
Definition at line 95 of file java_types.h.
|
inline |
Definition at line 595 of file java_types.h.
|
inline |
Check whether a reference to a typet is a Java generic parameter/variable, e.g., T in List<T>.
| base | Source type. |
type is a generic Java parameter type Definition at line 810 of file java_types.h.
|
inline |
Definition at line 939 of file java_types.h.
|
inline |
Definition at line 179 of file java_types.h.
|
inline |
Definition at line 624 of file java_types.h.
Compares the types, including checking element types if both types are arrays.
| type1 | First type to compare |
| type2 | Second type to compare |
Definition at line 895 of file java_types.cpp.
| std::string erase_type_arguments | ( | const std::string & | src | ) |
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
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
| src | The input string |
Definition at line 334 of file java_types.cpp.
| size_t find_closing_semi_colon_for_reference_type | ( | const std::string | src, |
| size_t | starting_point | ||
| ) |
Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point.
| src | The input string to work on. |
| starting_point | The string position where the opening 'L' we want to find the closing ';' for. |
Definition at line 516 of file java_types.cpp.
| std::string gather_full_class_name | ( | const std::string & | src | ) |
Returns the full class name, skipping over the generics.
This turns any of these:
com.package.OuterClass.Inner| src | a type descriptor or signature
|
Definition at line 365 of file java_types.cpp.
| std::vector<java_generic_parametert> get_all_generic_parameters | ( | const typet & | type | ) |
| type | Source type |
Definition at line 924 of file java_types.cpp.
| pointer | pointer to an array[reference] object |
Definition at line 206 of file java_types.cpp.
| pointer | pointer to an array[reference] object |
Definition at line 218 of file java_types.cpp.
| void get_dependencies_from_generic_parameters | ( | const std::string & | signature, |
| std::set< irep_idt > & | refs | ||
| ) |
Collect information about generic type parameters from a given signature.
This is used to get information about class dependencies that must be loaded but only appear as generic type argument, not as a field reference.
| signature | the string representation of the signature to analyze | |
| [out] | refs | the set to insert the names of the found dependencies |
Definition at line 996 of file java_types.cpp.
Collect information about generic type parameters from a given type.
This is used to get information about class dependencies that must be loaded but only appear as generic type argument, not as a field reference.
| t | the type to analyze | |
| [out] | refs | the set to insert the names of the found dependencies |
Definition at line 1032 of file java_types.cpp.
| bool is_java_array_tag | ( | const irep_idt & | tag | ) |
See above.
| tag | Tag of a struct |
Definition at line 233 of file java_types.cpp.
| bool is_java_array_type | ( | const typet & | type | ) |
Checks whether the given type is an array pointer type.
Definition at line 163 of file java_types.cpp.
|
inline |
| type | the type to check |
Definition at line 995 of file java_types.h.
|
inline |
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>.
| type | the type to check |
Definition at line 820 of file java_types.h.
|
inline |
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>.
| type | the type to check |
Definition at line 751 of file java_types.h.
|
inline |
| type | the type to check |
Definition at line 889 of file java_types.h.
|
inline |
| type | the type to check |
Definition at line 947 of file java_types.h.
|
inline |
| type | the type to check |
Definition at line 1100 of file java_types.h.
| 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.
Definition at line 179 of file java_types.cpp.
| bool is_valid_java_array | ( | const struct_typet & | type | ) |
Programmatic documentation of the structure of a Java array (of either primitives or references) type.
A Java array is represented in GOTO in the following way: A struct component with a tag like java::array[type] where type is either a primitive like int, or reference. The struct has precisely three components:
| type | A type that might represent a Java array |
Definition at line 838 of file java_types.cpp.
| 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.
If this is not an array type the return value will be {type, 0}.
Definition at line 189 of file java_types.cpp.
| 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.
| array_symbol | The java array type |
Definition at line 144 of file java_types.cpp.
| 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.
| array_symbol | The java array type |
Definition at line 154 of file java_types.cpp.
| java_reference_typet java_array_type | ( | const char | subtype | ) |
Construct an array pointer type.
It is a pointer to a symbol with identifier java::array[]. Its ID_element_type is set to the corresponding primitive type, or void* for arrays of references.
| subtype | Character indicating the type of array |
Definition at line 109 of file java_types.cpp.
| c_bool_typet java_boolean_type | ( | ) |
Definition at line 79 of file java_types.cpp.
| signedbv_typet java_byte_type | ( | ) |
Definition at line 55 of file java_types.cpp.
Java does not support byte/short return types. These are always promoted.
Definition at line 281 of file java_types.cpp.
Java does not support byte/short return types. These are always promoted.
Definition at line 269 of file java_types.cpp.
| char java_char_from_type | ( | const typet & | type | ) |
Definition at line 708 of file java_types.cpp.
| unsignedbv_typet java_char_type | ( | ) |
Definition at line 61 of file java_types.cpp.
| struct_tag_typet java_classname | ( | const std::string & | ) |
Definition at line 809 of file java_types.cpp.
| floatbv_typet java_double_type | ( | ) |
Definition at line 73 of file java_types.cpp.
| floatbv_typet java_float_type | ( | ) |
Definition at line 67 of file java_types.cpp.
Access information of the type bound of a generic java class type.
| index | the index of the type variable |
| t | the type from which to extract the type bound |
Definition at line 1051 of file java_types.h.
|
inline |
Access information of type variables of a generic java class type.
| index | the index of the type variable |
| type | the type from which to extract the type variable |
Definition at line 1037 of file java_types.h.
|
inline |
Access information of type arguments of java instantiated type.
| index | the index of the type argument |
| type | the type from which to extract the type argument |
Definition at line 1022 of file java_types.h.
| std::vector<typet> java_generic_type_from_string | ( | const std::string & | class_name, |
| const std::string & | src | ||
| ) |
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.
This also supports parsing of bounds in the form of <T:CBound> for classes or <T::IBound> for interfaces.
For example for HashMap<K, V> a vector with two elements would be returned
the class signature is of the form <TX:Bound_X;:BoundZ;TY:Bound_Y;> or of the form <TX::Bound_X;:BoundZ;TY:Bound_Y;> if Bound_X is an interface
Definition at line 749 of file java_types.cpp.
|
inline |
Get the index in the subtypes array for a given component.
| gen_types | The subtypes array. |
| identifier | The string identifier of the type of the component. |
Definition at line 1160 of file java_types.h.
| signedbv_typet java_int_type | ( | ) |
Definition at line 31 of file java_types.cpp.
| java_reference_typet java_lang_object_type | ( | ) |
Definition at line 98 of file java_types.cpp.
| signedbv_typet java_long_type | ( | ) |
Definition at line 43 of file java_types.cpp.
| java_reference_typet java_reference_array_type | ( | const struct_tag_typet & | element_type | ) |
Definition at line 541 of file java_types.cpp.
| java_reference_typet java_reference_type | ( | const struct_tag_typet & | subtype | ) |
Definition at line 93 of file java_types.cpp.
| reference_typet java_reference_type | ( | const typet & | subtype | ) |
Definition at line 88 of file java_types.cpp.
| signedbv_typet java_short_type | ( | ) |
Definition at line 49 of file java_types.cpp.
| typet java_type_from_char | ( | char | t | ) |
Constructs a type indicated by the given character:
Definition at line 248 of file java_types.cpp.
| optionalt<typet> java_type_from_string | ( | const std::string & | src, |
| const std::string & | class_name_prefix | ||
| ) |
Transforms a string representation of a Java type into an internal type representation thereof.
Example use are object types like "Ljava/lang/Integer;", type variables/parameters like "TE;" which require a non-empty class_name_prefix or generic types like "Ljava/util/List<TE;>;" or "Ljava/util/List<Ljava/lang/Integer;>;" also requiring class_name_prefix.
| src | the string representation as used in the class file |
| class_name_prefix | name of class to append to generic type variables/parameters |
Definition at line 561 of file java_types.cpp.
|
inline |
Definition at line 1141 of file java_types.h.
| empty_typet java_void_type | ( | ) |
Definition at line 37 of file java_types.cpp.
| std::vector<std::string> parse_raw_list_types | ( | const std::string | src, |
| const char | opening_bracket, | ||
| const char | closing_bracket | ||
| ) |
Given a substring of a descriptor or signature that contains one or more types parse out the individual type strings.
| src | The input string that is wrapped in either ( ) or < > |
| opening_bracket | For checking string is passed in as expected, the opening bracket (i.e. '(' or '<'). |
| closing_bracket | For checking string is passed in as expected, the closing bracket (i.e. ')' or '>'). |
Definition at line 419 of file java_types.cpp.
| std::string pretty_java_type | ( | const typet & | ) |
Definition at line 1089 of file java_types.cpp.
| std::string pretty_signature | ( | const java_method_typet & | ) |
Definition at line 1131 of file java_types.cpp.
|
inline |
Definition at line 84 of file java_types.h.
|
inline |
Definition at line 89 of file java_types.h.
|
inline |
Definition at line 582 of file java_types.h.
|
inline |
Definition at line 588 of file java_types.h.
|
inline |
| type | the type to check |
Definition at line 1003 of file java_types.h.
|
inline |
| type | source type |
Definition at line 1012 of file java_types.h.
|
inline |
| type | source type |
Definition at line 827 of file java_types.h.
|
inline |
| type | source type |
Definition at line 836 of file java_types.h.
|
inline |
| type | source type |
Definition at line 759 of file java_types.h.
|
inline |
| type | source type |
Definition at line 767 of file java_types.h.
|
inline |
| type | the type to convert |
Definition at line 897 of file java_types.h.
|
inline |
| type | the type to convert |
Definition at line 906 of file java_types.h.
|
inline |
| type | source type |
Definition at line 954 of file java_types.h.
|
inline |
| type | source type |
Definition at line 963 of file java_types.h.
|
inline |
| type | the type to check |
Definition at line 1108 of file java_types.h.
|
inline |
| type | source type |
Definition at line 1117 of file java_types.h.
|
inline |
Definition at line 184 of file java_types.h.
|
inline |
Definition at line 190 of file java_types.h.
|
inline |
Definition at line 630 of file java_types.h.
|
inline |
Definition at line 636 of file java_types.h.