9 #ifndef CPROVER_JAVA_BYTECODE_JAVA_TYPES_H 10 #define CPROVER_JAVA_BYTECODE_JAVA_TYPES_H 51 return static_cast<const typet &
>(
find(ID_type));
57 return reinterpret_cast<const std::vector<valuet> &
>(
get_sub());
63 return reinterpret_cast<std::vector<valuet> &
>(
get_sub());
73 return reinterpret_cast<const std::vector<java_annotationt> &
>(
80 return reinterpret_cast<std::vector<java_annotationt> &
>(
106 return get(ID_access);
111 return set(ID_access, access);
121 return set(ID_is_inner_class, is_inner_class);
126 return get(ID_outer_class);
131 return set(ID_outer_class, outer_class);
136 return get(ID_super_class);
141 return set(ID_super_class, super_class);
151 return set(ID_is_static, is_static_class);
161 return set(ID_is_anonymous, is_anonymous_class);
171 set(ID_final, is_final);
176 set(ID_incomplete_class,
true);
181 return get_bool(ID_incomplete_class);
200 return find(ID_java_lambda_method_handles).
get_sub();
205 return add(ID_java_lambda_method_handles).
get_sub();
248 assert(type.
id()==ID_struct);
254 assert(type.
id()==ID_struct);
276 set(ID_C_java_method_type,
true);
285 set(ID_C_java_method_type,
true);
290 std::vector<irep_idt> exceptions;
291 for(
const auto &e :
find(ID_exceptions_thrown_list).
get_sub())
292 exceptions.push_back(e.id());
308 set(ID_final, is_final);
313 return get_bool(ID_is_native_method);
318 set(ID_is_native_method, is_native);
323 return get_bool(ID_is_varargs_method);
328 set(ID_is_varargs_method, is_varargs);
335 return type.id() == ID_code && type.get_bool(ID_C_java_method_type);
372 const std::string &class_name_prefix=
"");
376 const std::string &);
381 const std::string src,
382 size_t starting_point = 0);
386 char opening_bracket,
387 char closing_bracket);
407 set(ID_C_java_generic_parameter,
true);
448 return type.
get_bool(ID_C_java_generic_parameter);
491 set(ID_C_java_generic_type,
true);
512 return is_reference(type) && type.get_bool(ID_C_java_generic_type);
549 set(ID_C_java_generics_class_type,
true);
567 return type.
get_bool(ID_C_java_generics_class_type);
596 const std::vector<reference_typet> &type_arguments =
599 return type_arguments[index];
609 const std::vector<java_generic_parametert> &gen_types=type.
generic_types();
614 return gen_type.type_variable().get_identifier();
626 const std::vector<java_generic_parametert> &gen_types=type.
generic_types();
631 return gen_type.subtype();
647 set(ID_C_java_implicitly_generic_class_type,
true);
648 for(
const auto &type : generic_types)
672 return type.
get_bool(ID_C_java_implicitly_generic_class_type);
700 "Unsupported class signature: "+type)
706 const std::string &descriptor,
708 const std::string &class_name)
725 const std::vector<java_generic_parametert> &gen_types,
728 const auto iter = std::find_if(
733 return ref.type_variable().get_identifier() == identifier;
736 if(iter == gen_types.cend())
741 return std::distance(gen_types.cbegin(), iter);
746 std::set<irep_idt> &);
749 std::set<irep_idt> &);
761 const std::string &base_ref,
762 const std::string &class_name_prefix);
782 return type.
get_bool(ID_C_java_generic_symbol);
821 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H generic_typest & generic_types()
std::vector< java_annotationt > & get_annotations()
The type of an expression, extends irept.
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...
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 ...
unsupported_java_class_signature_exceptiont(std::string type)
std::vector< java_generic_parametert > implicit_generic_typest
char java_char_from_type(const typet &type)
bool get_is_varargs() const
java_implicitly_generic_class_typet(const java_class_typet &class_type, const implicit_generic_typest &generic_types)
const irep_idt & get_identifier() const
bool get_is_anonymous_class() 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...
void set_is_final(bool is_final)
std::vector< valuet > & get_values()
bool is_multidim_java_array_type(const typet &type)
Checks whether the given type is a multi-dimensional array pointer type,.
const irep_idt & get_outer_class() const
bool get_is_inner_class() const
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
std::vector< irept > subt
void add_lambda_method_handle(const irep_idt &identifier)
const java_lambda_method_handlest & lambda_method_handles() const
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
bool is_java_generic_parameter(const typet &type)
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>. ...
struct_tag_typet java_classname(const std::string &)
bool can_cast_type< java_generic_typet >(const typet &type)
bool is_java_generic_struct_tag_type(const typet &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.
std::vector< parametert > parameterst
const java_generic_parametert & to_java_generic_parameter(const typet &type)
void set_final(bool is_final)
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
A struct tag type, i.e., struct_typet with an identifier.
std::string pretty_java_type(const typet &)
const generic_typest & generic_types() const
void get_dependencies_from_generic_parameters(const std::string &, std::set< irep_idt > &)
Collect information about generic type parameters from a given signature.
An exception that is raised for unsupported class signature.
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...
java_generic_typet(const typet &_type)
Structure type, corresponds to C style structs.
const std::vector< irep_idt > throws_exceptions() const
void set_access(const irep_idt &access)
bool get_bool(const irep_namet &name) const
java_generic_class_typet()
bool is_valid_java_array(const struct_typet &)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
optionalt< size_t > generic_type_index(const java_generic_parametert &type) const
Check if this symbol has the given generic type.
irept::subt java_lambda_method_handlest
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.
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...
valuet(irep_idt name, const exprt &value)
const irep_idt & get_super_class() const
const generic_type_argumentst & generic_type_arguments() const
java_method_typet(parameterst &&_parameters, typet &&_return_type)
Constructs a new code type, i.e.
const irep_idt & id() const
void set_outer_class(const irep_idt &outer_class)
void set_super_class(const irep_idt &super_class)
void set_native(bool is_native)
const type_variablet & type_variable() const
std::vector< reference_typet > generic_type_argumentst
bool is_java_array_tag(const irep_idt &tag)
See above.
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
const irep_idt & get_access() const
java_lambda_method_handlest & lambda_method_handles()
void add_throws_exceptions(irep_idt exception)
const exprt & get_value() const
void set_is_inner_class(const bool &is_inner_class)
bool get_is_final() const
implicit_generic_typest & implicit_generic_types()
const std::vector< java_annotationt > & get_annotations() const
struct_tag_typet type_variablet
nonstd::optional< T > optionalt
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
API to expression classes.
bool is_reference(const typet &type)
Returns true if the type is a reference.
std::string pretty_signature(const java_method_typet &)
bool can_cast_type< java_class_typet >(const typet &type)
typet java_bytecode_promotion(const typet &)
Java does not support byte/short return types. These are always promoted.
void add_unknown_lambda_method_handle()
#define PRECONDITION(CONDITION)
const java_generic_struct_tag_typet & to_java_generic_struct_tag_type(const typet &type)
Base class for tree-like data structures with sharing.
java_generic_parametert(const irep_idt &_type_var_name, const struct_tag_typet &_bound)
bool is_java_generic_class_type(const typet &type)
bool can_cast_type< annotated_typet >(const typet &)
bool can_cast_type< java_method_typet >(const typet &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.
reference_typet java_lang_object_type()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
const implicit_generic_typest & implicit_generic_types() const
bool get_is_static_class() const
const typet & java_generic_get_inst_type(size_t index, const java_generic_typet &type)
Access information of type arguments of java instantiated type.
typet java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
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...
const irep_idt & get_name() const
Type for a generic symbol, extends struct_tag_typet with a vector of java generic types...
const java_generic_typet & to_java_generic_type(const typet &type)
const type_variablest & type_variables() const
const java_method_typet & to_java_method_type(const typet &type)
void set_is_varargs(bool is_varargs)
std::vector< type_variablet > type_variablest
type_variablest & type_variables()
void set_is_stub(const bool &is_stub)
Base class for all expressions.
void set_is_static_class(const bool &is_static_class)
std::vector< java_annotationt > & get_annotations()
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
std::vector< reference_typet > generic_typest
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>...
typet java_boolean_type()
void set_is_anonymous_class(const bool &is_anonymous_class)
const irep_idt get_name() const
java_method_typet(parameterst &&_parameters, const typet &_return_type)
Constructs a new code type, i.e.
java_annotationt(const typet &type)
irept & add(const irep_namet &name)
std::string gather_full_class_name(const std::string &)
Returns the full class name, skipping over the generics.
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.
generic_typest & generic_types()
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.
java_generic_struct_tag_typet(const struct_tag_typet &type, const std::string &base_ref, const std::string &class_name_prefix)
Construct a generic symbol type by extending the symbol type type with generic types extracted from t...
generic_type_argumentst & generic_type_arguments()
const std::vector< valuet > & get_values() const
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
bool is_java_generic_type(const typet &type)
const typet & get_type() const
reference_typet java_reference_type(const typet &subtype)
bool is_java_implicitly_generic_class_type(const typet &type)
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
const std::vector< java_annotationt > & get_annotations() const
Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class o...
type_variablet & type_variable_ref()
const irept & find(const irep_namet &name) const
const annotated_typet & to_annotated_type(const typet &type)
bool can_cast_type< class_typet >(const typet &type)
Check whether a reference to a typet is a class_typet.
const java_class_typet & to_java_class_type(const typet &type)
const generic_typest & generic_types() const
std::vector< java_generic_parametert > generic_typest
Defines typet, type_with_subtypet and type_with_subtypest.