cprover
|
#include <util/invariant.h>
#include <algorithm>
#include <set>
#include <util/type.h>
#include <util/std_types.h>
#include <util/c_types.h>
#include <util/optional.h>
#include <util/std_expr.h>
Go to the source code of this file.
Classes | |
class | java_annotationt |
class | java_annotationt::valuet |
class | annotated_typet |
class | java_class_typet |
class | java_generic_parametert |
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T> . More... | |
class | java_generic_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_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... | |
class | java_generic_symbol_typet |
Type for a generic symbol, extends symbol_typet with a vector of java generic types. More... | |
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 &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) |
typet | java_int_type () |
typet | java_long_type () |
typet | java_short_type () |
typet | java_byte_type () |
typet | java_char_type () |
typet | java_float_type () |
typet | java_double_type () |
typet | java_boolean_type () |
reference_typet | java_reference_type (const typet &subtype) |
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) |
Return the type of the elements of a given java array type. More... | |
bool | is_reference_type (char t) |
typet | java_type_from_char (char t) |
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... | |
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 (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_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) |
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... | |
bool | is_java_generic_symbol_type (const typet &type) |
const java_generic_symbol_typet & | to_java_generic_symbol_type (const typet &type) |
java_generic_symbol_typet & | to_java_generic_symbol_type (typet &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 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 code_typet &) |
|
inline |
Definition at line 96 of file java_types.h.
|
inline |
Definition at line 176 of file java_types.h.
References can_cast_type< class_typet >().
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 733 of file java_types.cpp.
References equal_java_types(), symbol_typet::get_identifier(), irept::id(), is_java_array_tag(), java_array_element_type(), typet::subtype(), and to_symbol_type().
Referenced by equal_java_types(), and java_object_factoryt::gen_nondet_pointer_init().
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 231 of file java_types.cpp.
References find_closing_delimiter().
Referenced by gather_full_class_name(), and get_dependencies_from_generic_parameters().
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 390 of file java_types.cpp.
References find_closing_delimiter(), INVARIANT, and PRECONDITION.
Referenced by extract_generic_interface_reference(), extract_generic_superclass_reference(), and parse_list_types().
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 262 of file java_types.cpp.
References erase_type_arguments(), and PRECONDITION.
Referenced by build_class_name().
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 |
refs | [out]: the set to insert the names of the found dependencies |
Definition at line 805 of file java_types.cpp.
References erase_type_arguments(), get_dependencies_from_generic_parameters_rec(), java_generic_type_from_string(), and java_type_from_string().
Referenced by java_bytecode_parsert::get_class_refs(), get_dependencies_from_generic_parameters_rec(), and java_bytecode_parsert::rclass_attribute().
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 |
refs | [out]: the set to insert the names of the found dependencies |
Definition at line 841 of file java_types.cpp.
References get_dependencies_from_generic_parameters_rec().
bool is_java_array_tag | ( | const irep_idt & | tag | ) |
See above.
Definition at line 137 of file java_types.cpp.
References has_prefix(), and id2string().
Referenced by equal_java_types(), ci_lazy_methods_neededt::gather_field_types(), get_dependencies_from_generic_parameters_rec(), ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(), java_array_element_type(), java_is_array_type(), java_static_lifetime_init(), pretty_java_type(), require_goto_statements::require_struct_array_component_assignment(), and select_pointer_typet::specialize_generics().
|
inline |
type | the type to check |
Definition at line 398 of file java_types.h.
References irept::get_bool().
Referenced by get_all_generic_parameters(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(), java_generic_class_type_bound(), require_type::require_java_generic_class(), require_type::require_java_non_generic_class(), and to_java_generic_class_type().
|
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 281 of file java_types.h.
References irept::get_bool().
Referenced by java_generic_symbol_typet::generic_type_index(), select_pointer_typet::get_recursively_instantiated_type(), ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(), generic_parameter_specialization_map_keyst::insert_pairs(), require_type::require_java_generic_class(), require_type::require_java_generic_parameter(), require_java_generic_type_argument_expectation(), require_type::require_java_implicitly_generic_class(), require_type::require_java_non_generic_type(), select_pointer_typet::specialize_generics(), and to_java_generic_parameter().
|
inline |
type | the type to check |
Definition at line 613 of file java_types.h.
References irept::get_bool().
Referenced by generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(), require_type::require_java_generic_symbol_type(), and to_java_generic_symbol_type().
|
inline |
type | the type to check |
Definition at line 346 of file java_types.h.
References irept::get_bool().
Referenced by get_dependencies_from_generic_parameters_rec(), ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), java_generic_symbol_typet::java_generic_symbol_typet(), require_type::require_java_generic_type(), require_type::require_java_non_generic_type(), and to_java_generic_type().
|
inline |
type | the type to check |
Definition at line 503 of file java_types.h.
References irept::get_bool().
Referenced by get_all_generic_parameters(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(), require_type::require_java_implicitly_generic_class(), require_type::require_java_non_generic_class(), and to_java_implicitly_generic_class_type().
bool is_reference_type | ( | char | t | ) |
Definition at line 142 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 696 of file java_types.cpp.
References struct_union_typet::components(), struct_union_typet::componentt::get_name(), irept::id(), java_int_type(), and exprt::type().
Referenced by java_object_factoryt::gen_nondet_array_init().
typet java_array_element_type | ( | const symbol_typet & | array_type | ) |
Return the type of the elements of a given java array type.
array_type | The java array type |
Definition at line 126 of file java_types.cpp.
References typet::find_type(), symbol_typet::get_identifier(), INVARIANT, and is_java_array_tag().
Referenced by equal_java_types(), ci_lazy_methods_neededt::gather_field_types(), get_dependencies_from_generic_parameters_rec(), pretty_java_type(), and select_pointer_typet::specialize_generics().
reference_typet java_array_type | ( | const char | subtype | ) |
Definition at line 90 of file java_types.cpp.
References id2string(), java_reference_type(), java_type_from_char(), irept::set(), and UNREACHABLE.
Referenced by java_bytecode_convert_methodt::convert_aload(), java_bytecode_convert_methodt::convert_astore(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_newarray(), java_type_from_string(), and select_pointer_typet::specialize_generics().
typet java_boolean_type | ( | ) |
Definition at line 72 of file java_types.cpp.
Referenced by constant_bool(), java_bytecode_convert_methodt::convert_invoke(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_bytecode_promotion(), java_root_class(), java_static_lifetime_init(), java_type_from_char(), java_type_from_string(), java_string_library_preprocesst::make_string_format_code(), and pretty_java_type().
typet java_byte_type | ( | ) |
Definition at line 52 of file java_types.cpp.
Referenced by expr2javat::convert_constant(), java_bytecode_convert_methodt::convert_invoke(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_bytecode_promotion(), java_char_from_type(), java_type_from_char(), java_type_from_string(), and pretty_java_type().
Java does not support byte/short return types. These are always promoted.
Definition at line 166 of file java_types.cpp.
References java_boolean_type(), java_byte_type(), java_char_type(), java_int_type(), and java_short_type().
Referenced by java_bytecode_convert_methodt::convert_aload(), java_bytecode_convert_methodt::convert_getstatic(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), and java_bytecode_promotion().
Java does not support byte/short return types. These are always promoted.
Definition at line 178 of file java_types.cpp.
References java_bytecode_promotion(), and exprt::type().
char java_char_from_type | ( | const typet & | type | ) |
Definition at line 569 of file java_types.cpp.
References bitvector_typet::get_width(), irept::id(), java_byte_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_short_type(), to_floatbv_type(), and to_signedbv_type().
Referenced by java_bytecode_convert_methodt::convert(), and java_bytecode_initialize_parameter_names().
typet java_char_type | ( | ) |
Definition at line 57 of file java_types.cpp.
Referenced by java_string_library_preprocesst::add_string_type(), expr2javat::convert_constant(), java_bytecode_convert_methodt::convert_invoke(), expr2javat::convert_rec(), java_string_library_preprocesst::decl_string_expr(), java_string_library_preprocesst::get_primitive_value_of_object(), initialize_nondet_string_struct(), java_bytecode_promotion(), java_type_from_char(), java_type_from_string(), make_nondet_infinite_char_array(), java_string_library_preprocesst::make_string_format_code(), pretty_java_type(), java_string_library_preprocesst::replace_char_array(), and utf16_to_array().
symbol_typet java_classname | ( | const std::string & | ) |
Definition at line 668 of file java_types.cpp.
References java_type_from_string(), irept::set(), slash_to_dot(), and to_symbol_type().
Referenced by java_bytecode_parsert::rconstant_pool().
typet java_double_type | ( | ) |
Definition at line 67 of file java_types.cpp.
References ieee_float_spect::double_precision(), and ieee_float_spect::to_type().
Referenced by expr2javat::convert_constant(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_char_from_type(), java_type_from_char(), java_type_from_string(), and pretty_java_type().
typet java_float_type | ( | ) |
Definition at line 62 of file java_types.cpp.
References ieee_float_spect::single_precision(), and ieee_float_spect::to_type().
Referenced by expr2javat::convert_constant(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_char_from_type(), java_type_from_char(), java_type_from_string(), java_string_library_preprocesst::make_string_format_code(), and pretty_java_type().
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 454 of file java_types.h.
References java_generic_class_typet::generic_types(), is_java_generic_class_type(), PRECONDITION, to_java_class_type(), and to_java_generic_class_type().
|
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 440 of file java_types.h.
References java_generic_class_typet::generic_types(), and PRECONDITION.
|
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 425 of file java_types.h.
References java_generic_typet::generic_type_arguments(), and PRECONDITION.
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 610 of file java_types.cpp.
References find_closing_delimiter(), INVARIANT, java_type_from_string(), PRECONDITION, and to_symbol_type().
Referenced by java_bytecode_convert_classt::convert(), and get_dependencies_from_generic_parameters().
|
inline |
Get the index in the subtypes array for a given component.
t | The type we search for the subtypes in. |
identifier | The string identifier of the type of the component. |
Definition at line 557 of file java_types.h.
typet java_int_type | ( | ) |
Definition at line 32 of file java_types.cpp.
Referenced by add_array_to_length_association(), add_character_set_constraint(), add_pointer_to_array_association(), java_object_factoryt::allocate_nondet_length_array(), java_bytecode_instrumentt::check_array_access(), java_bytecode_instrumentt::check_array_length(), java_bytecode_convert_methodt::convert_cmp(), java_bytecode_convert_methodt::convert_cmp2(), java_bytecode_convert_methodt::convert_iinc(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_multianewarray(), java_bytecode_convert_methodt::convert_newarray(), expr2javat::convert_rec(), java_object_factoryt::gen_nondet_array_init(), java_string_library_preprocesst::get_object_at_index(), get_or_create_string_literal_symbol(), java_string_library_preprocesst::get_primitive_value_of_object(), initialize_nondet_string_struct(), instrument_getCurrentThreadID(), instrument_start_thread(), is_valid_java_array(), java_bytecode_promotion(), java_char_from_type(), java_type_from_char(), java_type_from_string(), make_nondet_infinite_char_array(), java_string_library_preprocesst::make_nondet_string_expr(), java_string_library_preprocesst::make_object_get_class_code(), java_string_library_preprocesst::make_string_format_code(), pretty_java_type(), java_bytecode_parsert::rconstant_pool(), java_string_library_preprocesst::replace_char_array(), java_string_library_preprocesst::string_expr_of_function(), string_length_type(), and utf16_to_array().
reference_typet java_lang_object_type | ( | ) |
Definition at line 85 of file java_types.cpp.
References java_reference_type().
Referenced by remove_instanceoft::lower_instanceof().
typet java_long_type | ( | ) |
Definition at line 42 of file java_types.cpp.
Referenced by expr2javat::convert_constant(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_char_from_type(), java_type_from_char(), java_type_from_string(), pretty_java_type(), and java_bytecode_parsert::rconstant_pool().
reference_typet java_reference_type | ( | const typet & | subtype | ) |
Definition at line 80 of file java_types.cpp.
References reference_type().
Referenced by build_class_name(), java_bytecode_convert_methodt::convert_ifnonull(), java_bytecode_convert_methodt::convert_ifnull(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), java_bytecode_convert_methodt::convert_monitorenter(), java_bytecode_convert_methodt::convert_monitorexit(), java_bytecode_convert_methodt::convert_multianewarray(), java_bytecode_convert_methodt::convert_new(), generate_java_start_function(), java_array_type(), java_bytecode_convert_method_lazy(), java_lang_object_type(), java_type_from_char(), java_string_library_preprocesst::make_argument_for_format(), java_string_library_preprocesst::make_object_get_class_code(), and to_member().
typet java_short_type | ( | ) |
Definition at line 47 of file java_types.cpp.
Referenced by expr2javat::convert_constant(), java_bytecode_convert_methodt::convert_invoke(), expr2javat::convert_rec(), java_string_library_preprocesst::get_primitive_value_of_object(), java_bytecode_promotion(), java_char_from_type(), java_type_from_char(), java_type_from_string(), and pretty_java_type().
typet java_type_from_char | ( | char | t | ) |
Definition at line 147 of file java_types.cpp.
References java_boolean_type(), java_byte_type(), java_char_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_reference_type(), java_short_type(), and UNREACHABLE.
Referenced by java_bytecode_convert_methodt::convert_aload(), java_bytecode_convert_methodt::convert_astore(), java_bytecode_convert_methodt::convert_const(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_ushr(), java_array_type(), and java_bytecode_convert_methodt::variable().
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 428 of file java_types.cpp.
References build_class_name(), find_closing_delimiter(), irept::id(), INVARIANT, java_array_type(), java_boolean_type(), java_byte_type(), java_char_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_short_type(), java_type_from_string(), java_void_type(), parse_list_types(), PRECONDITION, irept::set(), typet::subtype(), and to_symbol_type().
Referenced by java_bytecode_convert_methodt::convert(), java_bytecode_parsert::get_class_refs(), get_dependencies_from_generic_parameters(), is_java_main(), java_classname(), java_generic_symbol_typet::java_generic_symbol_typet(), java_generic_type_from_string(), java_type_from_string(), java_type_from_string_with_exception(), member_type_lazy(), parse_list_types(), java_bytecode_convert_methodt::setup_local_variables(), and java_bytecode_parsert::type_entry().
|
inline |
Definition at line 538 of file java_types.h.
References java_type_from_string().
Referenced by java_bytecode_convert_methodt::convert(), and java_bytecode_parsert::get_class_refs().
std::string pretty_java_type | ( | const typet & | ) |
Definition at line 897 of file java_types.cpp.
References irept::id(), id2string(), is_java_array_tag(), is_reference(), java_array_element_type(), java_boolean_type(), java_byte_type(), java_char_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_short_type(), pretty_java_type(), strip_java_namespace_prefix(), typet::subtype(), and to_symbol_type().
Referenced by pretty_java_type(), and pretty_signature().
std::string pretty_signature | ( | const code_typet & | ) |
Definition at line 935 of file java_types.cpp.
References code_typet::parameters(), and pretty_java_type().
Referenced by java_bytecode_convert_methodt::convert(), and java_bytecode_convert_method_lazy().
|
inline |
Definition at line 85 of file java_types.h.
|
inline |
Definition at line 90 of file java_types.h.
|
inline |
Definition at line 163 of file java_types.h.
References irept::id().
Referenced by java_bytecode_convert_methodt::convert(), java_bytecode_languaget::convert_single_method(), get_all_generic_parameters(), java_generic_class_type_bound(), require_type::require_java_generic_class(), require_type::require_java_implicitly_generic_class(), and require_type::require_java_non_generic_class().
|
inline |
Definition at line 169 of file java_types.h.
References irept::id().
|
inline |
type | the type to check |
Definition at line 406 of file java_types.h.
References is_java_generic_class_type(), and PRECONDITION.
Referenced by get_all_generic_parameters(), java_generic_class_type_bound(), and require_type::require_java_generic_class().
|
inline |
type | source type |
Definition at line 415 of file java_types.h.
References is_java_generic_class_type(), and PRECONDITION.
|
inline |
type | source type |
Definition at line 288 of file java_types.h.
References is_java_generic_parameter(), and PRECONDITION.
Referenced by java_bytecode_convert_classt::convert(), java_generic_symbol_typet::generic_type_index(), select_pointer_typet::get_recursively_instantiated_type(), generic_parameter_specialization_map_keyst::insert_pairs(), require_type::require_java_generic_parameter(), require_java_generic_type_argument_expectation(), and select_pointer_typet::specialize_generics().
|
inline |
type | source type |
Definition at line 297 of file java_types.h.
References is_java_generic_parameter(), and PRECONDITION.
|
inline |
type | the type to convert |
Definition at line 621 of file java_types.h.
References is_java_generic_symbol_type(), and PRECONDITION.
Referenced by generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(), and require_type::require_java_generic_symbol_type().
|
inline |
type | the type to convert |
Definition at line 629 of file java_types.h.
References is_java_generic_symbol_type(), and PRECONDITION.
|
inline |
type | source type |
Definition at line 353 of file java_types.h.
References irept::id(), is_java_generic_type(), and PRECONDITION.
Referenced by get_dependencies_from_generic_parameters_rec(), ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), java_generic_symbol_typet::java_generic_symbol_typet(), and require_type::require_java_generic_type().
|
inline |
type | source type |
Definition at line 364 of file java_types.h.
References irept::id(), is_java_generic_type(), and PRECONDITION.
|
inline |
type | the type to check |
Definition at line 511 of file java_types.h.
References is_java_implicitly_generic_class_type(), and PRECONDITION.
Referenced by get_all_generic_parameters(), and require_type::require_java_implicitly_generic_class().
|
inline |
type | source type |
Definition at line 520 of file java_types.h.
References is_java_implicitly_generic_class_type(), and PRECONDITION.