Go to the documentation of this file.
9 #ifndef CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
10 #define CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
52 return static_cast<const typet &
>(
find(ID_type));
58 return reinterpret_cast<const std::vector<valuet> &
>(
get_sub());
64 return reinterpret_cast<std::vector<valuet> &
>(
get_sub());
74 return reinterpret_cast<const std::vector<java_annotationt> &
>(
81 return reinterpret_cast<std::vector<java_annotationt> &
>(
112 :
code_typet(std::move(_parameters), std::move(_return_type))
114 set(ID_C_java_method_type,
true);
121 :
code_typet(std::move(_parameters), _return_type)
123 set(ID_C_java_method_type,
true);
128 std::vector<irep_idt> exceptions;
129 for(
const auto &e :
find(ID_exceptions_thrown_list).
get_sub())
130 exceptions.push_back(e.id());
146 set(ID_final, is_final);
151 return get_bool(ID_is_native_method);
156 set(ID_is_native_method, is_native);
161 return get_bool(ID_is_varargs_method);
166 set(ID_is_varargs_method, is_varargs);
183 return type.
id() == ID_code && type.
get_bool(ID_C_java_method_type);
220 set(ID_final, is_final);
272 set(ID_final, is_final);
278 return get_bool(ID_is_native_method);
284 set(ID_is_native_method, is_native);
315 return get(ID_access);
320 return set(ID_access, access);
330 return set(ID_is_inner_class, is_inner_class);
335 return get(ID_outer_class);
340 return set(ID_outer_class, outer_class);
345 return get(ID_super_class);
350 return set(ID_super_class, super_class);
360 return set(ID_is_static, is_static_class);
370 return set(ID_is_anonymous, is_anonymous_class);
380 set(ID_final, is_final);
385 set(ID_incomplete_class, is_stub);
390 return get_bool(ID_incomplete_class);
402 set(ID_enumeration, is_enumeration);
414 set(ID_abstract,
abstract);
426 set(ID_synthetic, synthetic);
438 set(ID_is_annotation, is_annotation);
450 set(ID_interface, interface);
469 return find(ID_java_lambda_method_handles).
get_sub();
474 return add(ID_java_lambda_method_handles).
get_sub();
496 return type_checked_cast<annotated_typet>(
497 static_cast<typet &
>(*
this)).get_annotations();
517 return get(ID_inner_name);
523 set(ID_inner_name, name);
529 assert(type.
id()==ID_struct);
535 assert(type.
id()==ID_struct);
571 return type.
id() == ID_pointer &&
601 #define JAVA_REFERENCE_ARRAY_CLASSID "java::array[reference]"
611 std::pair<typet, std::size_t>
614 #define JAVA_ARRAY_DIMENSION_FIELD_NAME "@array_dimensions"
616 #define JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME "@element_class_identifier"
622 const std::string &class_name_prefix =
"");
626 const std::string &);
631 const std::string src,
632 size_t starting_point = 0);
636 char opening_bracket,
637 char closing_bracket);
657 set(ID_C_java_generic_parameter,
true);
698 return type.
get_bool(ID_C_java_generic_parameter);
809 set(ID_C_java_generic_symbol,
true);
814 const std::string &base_ref,
815 const std::string &class_name_prefix);
835 return type.
get_bool(ID_C_java_generic_symbol);
922 set(ID_C_java_generics_class_type,
true);
940 return type.
get_bool(ID_C_java_generics_class_type);
969 const std::vector<reference_typet> &type_arguments =
972 return type_arguments[index];
982 const std::vector<java_generic_parametert> &gen_types=type.
generic_types();
999 const std::vector<java_generic_parametert> &gen_types=type.
generic_types();
1020 set(ID_C_java_implicitly_generic_class_type,
true);
1021 for(
const auto &type : generic_types)
1045 return type.
get_bool(ID_C_java_implicitly_generic_class_type);
1069 std::vector<java_generic_parametert>
1079 "Unsupported class signature: "+type)
1085 const std::string &descriptor,
1087 const std::string &class_name)
1104 const std::vector<java_generic_parametert> &gen_types,
1107 const auto iter = std::find_if(
1112 return ref.type_variable().get_identifier() == identifier;
1115 if(iter == gen_types.cend())
1120 return narrow_cast<size_t>(std::distance(gen_types.cbegin(), iter));
1124 const std::string &,
1125 std::set<irep_idt> &);
1128 std::set<irep_idt> &);
1148 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
const irep_idt & get_identifier() const
bool is_java_generic_class_type(const typet &type)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool can_cast_type< java_reference_typet >(const typet &type)
java_generic_typet(const typet &_type)
struct_tag_typet(const irep_idt &identifier)
void add_throws_exception(irep_idt exception)
const typet & subtype() const
const irep_idt & get_inner_name() const
Get the name of a java inner class.
floatbv_typet java_double_type()
Reference that points to a java_generic_struct_tag_typet.
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool get_is_final() const
void set_synthetic(bool synthetic)
marks class synthetic
signedbv_typet java_byte_type()
void set_is_static_class(const bool &is_static_class)
void set_is_anonymous_class(const bool &is_anonymous_class)
bool can_cast_type< annotated_typet >(const typet &)
bool get_interface() const
is class an interface?
const implicit_generic_typest & implicit_generic_types() const
std::vector< java_generic_parametert > generic_typest
The type of an expression, extends irept.
std::vector< parametert > parameterst
const irep_idt & get_name() const
bool get_is_enumeration() const
is class an enumeration?
const componentt & get_component(const irep_idt &component_name) const
An exception that is raised for unsupported class signature.
bool get_is_native() const
is a method 'native'?
signedbv_typet java_int_type()
methodt(const irep_idt &_name, java_method_typet _type)
signedbv_typet java_long_type()
void add_unknown_lambda_method_handle()
bool is_synthetic() const
irept & add(const irep_namet &name)
Fixed-width bit-vector with IEEE floating-point interpretation.
const annotated_typet & to_annotated_type(const typet &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 ...
bool is_java_array_tag(const irep_idt &tag)
See above.
const irept & find(const irep_namet &name) const
std::vector< java_annotationt > & get_annotations()
java_method_typet & type()
Reference that points to a java_generic_parameter_tagt.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Base class for all expressions.
std::vector< componentt > componentst
A struct tag type, i.e., struct_typet with an identifier.
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.
void set_is_annotation(bool is_annotation)
marks class an annotation
bool can_cast_type< java_generic_typet >(const typet &type)
bool is_java_implicitly_generic_class_type(const typet &type)
const static_memberst & static_members() const
struct_tag_typet type_variablet
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
std::string pretty_java_type(const typet &)
generic_typest & generic_types()
std::string gather_full_class_name(const std::string &)
Returns the full class name, skipping over the generics.
const methodst & methods() const
void set_is_varargs(bool is_varargs)
java_generic_struct_tag_typet::generic_typest generic_type_argumentst
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
optionalt< size_t > generic_type_index(const java_generic_parametert &type) const
Check if this symbol has the given generic type.
valuet(irep_idt name, const exprt &value)
const generic_typest & generic_types() const
java_generic_class_typet()
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.
bool get_is_inner_class() const
std::string pretty_signature(const java_method_typet &)
Fixed-width bit-vector with unsigned binary interpretation.
type_variablet & type_variable_ref()
void set_inner_name(const irep_idt &name)
Set the name of a java inner class.
const generic_typest & generic_types() const
exprt get_array_dimension_field(const exprt &pointer)
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.
optionalt< typet > java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
const typet & java_generic_get_inst_type(size_t index, const java_generic_typet &type)
Access information of type arguments of java instantiated type.
java_reference_typet java_array_type(const char subtype)
Construct an array pointer type.
java_generic_parameter_tagt(const irep_idt &_type_var_name, const struct_tag_typet &_bound)
void set_is_enumeration(const bool is_enumeration)
marks class as an enumeration
typet & type()
Return the type of the expression.
bool get_is_anonymous_class() const
const java_method_typet & type() const
bool get_bool(const irep_namet &name) const
const std::vector< valuet > & get_values() const
void set_native(bool is_native)
const irep_idt get_name() const
java_annotationt(const typet &type)
const std::vector< java_annotationt > & get_annotations() const
struct_tag_typet & subtype()
componentst static_memberst
java_generic_struct_tag_typet(const struct_tag_typet &type)
bool get_is_annotation() const
is class an annotation?
const java_generic_struct_tag_typet & to_java_generic_struct_tag_type(const typet &type)
const generic_type_argumentst & generic_type_arguments() const
empty_typet java_void_type()
type_variablest & type_variables()
std::vector< java_generic_parametert > get_all_generic_parameters(const typet &type)
void set_is_final(const bool is_final)
is a method 'final'?
#define PRECONDITION(CONDITION)
bool is_java_generic_parameter(const typet &type)
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>.
java_generic_parametert(const irep_idt &_type_var_name, const struct_tag_typet &_bound)
Fixed-width bit-vector with two's complement interpretation.
const java_reference_typet & to_java_reference_type(const typet &type)
bool is_java_generic_struct_tag_type(const typet &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_type(const typet &type)
const static_memberst & static_members() const
Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class o...
implicit_generic_typest & implicit_generic_types()
generic_type_argumentst & generic_type_arguments()
void set_is_native(const bool is_native)
marks a method as 'native'
const type_variablest & type_variables() const
java_method_typet(parameterst &&_parameters, typet &&_return_type)
Constructs a new code type, i.e.
bool get_synthetic() const
is class synthetic?
const irep_idt & id() const
bool can_cast_type< java_class_typet >(const typet &type)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
componentst & components()
signedbv_typet java_short_type()
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>.
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>.
exprt get_array_element_type_field(const exprt &pointer)
const typet & get_type() const
bool get_abstract() const
is class abstract?
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
const java_generic_typet & to_java_generic_type(const typet &type)
nonstd::optional< T > optionalt
type_variablet & type_variable_ref()
typet java_bytecode_promotion(const typet &)
Java does not support byte/short return types. These are always promoted.
void set_final(bool is_final)
const type_variablet & type_variable() const
void set_interface(bool interface)
marks class an interface
void set_outer_class(const irep_idt &outer_class)
irept::subt java_lambda_method_handlest
componentt(const irep_idt &_name, typet _type)
const exprt & get_value() const
const irep_idt & get_name() const
Get the name of the struct, which can be used to look up its symbol in the symbol table.
std::vector< java_annotationt > & get_annotations()
void set_is_stub(bool is_stub)
void set_super_class(const irep_idt &super_class)
std::vector< reference_typet > generic_typest
void set_is_final(bool is_final)
const componentst & components() const
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.
java_lambda_method_handlest & lambda_method_handles()
bool get_is_final() const
is a method 'final'?
struct_tag_typet type_variablet
void set_access(const irep_idt &access)
java_reference_typet(const struct_tag_typet &_subtype, std::size_t _width)
bool is_valid_java_array(const struct_typet &)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
Structure type, corresponds to C style structs.
const struct_tag_typet & subtype() const
java_implicitly_generic_class_typet(const java_class_typet &class_type, const implicit_generic_typest &generic_types)
const java_generic_parametert & to_java_generic_parameter(const typet &type)
std::vector< java_generic_parametert > implicit_generic_typest
const irep_idt & get_outer_class() const
bool is_reference(const typet &type)
Returns true if the type is a reference.
const irep_idt & get(const irep_namet &name) const
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 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 java_generic_parameter_tagt & to_java_generic_parameter_tag(const typet &type)
void set(const irep_namet &name, const irep_idt &value)
std::vector< type_variablet > type_variablest
java_reference_typet java_reference_type(const struct_tag_typet &subtype)
void get_dependencies_from_generic_parameters(const std::string &, std::set< irep_idt > &)
Collect information about generic type parameters from a given signature.
generic_typest & generic_types()
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< 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 ...
std::vector< valuet > & get_values()
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 no...
void add_lambda_method_handle(const irep_idt &identifier)
void set_is_inner_class(const bool &is_inner_class)
unsignedbv_typet java_char_type()
bool can_cast_type< java_method_typet >(const typet &type)
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table.
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
java_reference_typet java_reference_array_type(const struct_tag_typet &element_type)
java_method_typet(parameterst &&_parameters, const typet &_return_type)
Constructs a new code type, i.e.
bool get_is_final() const
is a field 'final'?
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
bool get_is_varargs() const
void set_is_synthetic(bool is_synthetic)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irep_idt get_name() const
void set_abstract(bool abstract)
marks class abstract
void set_is_final(const bool is_final)
is a field 'final'?
This is a specialization of reference_typet.
unsupported_java_class_signature_exceptiont(std::string type)
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
const java_class_typet & to_java_class_type(const typet &type)
const irep_idt & get_super_class() const
const java_method_typet & to_java_method_type(const typet &type)
const std::vector< java_annotationt > & get_annotations() const
bool can_cast_type< class_typet >(const typet &type)
Check whether a reference to a typet is a class_typet.
const java_lambda_method_handlest & lambda_method_handles() const
struct_tag_typet java_classname(const std::string &)
const irep_idt & get_access() const
floatbv_typet java_float_type()
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.
const std::vector< irep_idt > throws_exceptions() const
static_memberst & static_members()
c_bool_typet java_boolean_type()
const type_variablet & type_variable() const
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 individu...
bool get_is_static_class() const
java_reference_typet java_lang_object_type()
char java_char_from_type(const typet &type)