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 set(ID_final, is_final);
129 ID_java_lambda_method_handles)
165 assert(type.
id()==ID_struct);
171 assert(type.
id()==ID_struct);
211 const std::string &class_name_prefix=
"");
215 const std::string &);
220 const std::string src,
221 size_t starting_point = 0);
242 set(ID_C_java_generic_parameter,
true);
283 return type.
get_bool(ID_C_java_generic_parameter);
326 set(ID_C_java_generic_type,
true);
348 return type.
get_bool(ID_C_java_generic_type);
357 type.
id()==ID_pointer &&
367 type.
id()==ID_pointer &&
382 set(ID_C_java_generics_class_type,
true);
400 return type.
get_bool(ID_C_java_generics_class_type);
429 const std::vector<reference_typet> &type_arguments =
432 return type_arguments[index];
442 const std::vector<java_generic_parametert> &gen_types=type.
generic_types();
447 return gen_type.type_variable().get_identifier();
459 const std::vector<java_generic_parametert> &gen_types=type.
generic_types();
464 return gen_type.subtype();
480 set(ID_C_java_implicitly_generic_class_type,
true);
481 for(
const auto &type : generic_types)
505 return type.
get_bool(ID_C_java_implicitly_generic_class_type);
533 "Unsupported class signature: "+type)
539 const std::string &descriptor,
541 const std::string &class_name)
558 const std::vector<java_generic_parametert> &gen_types,
561 const auto iter = std::find_if(
566 return ref.type_variable().get_identifier() == identifier;
569 if(iter == gen_types.cend())
574 return std::distance(gen_types.cbegin(), iter);
579 std::set<irep_idt> &);
582 std::set<irep_idt> &);
594 const std::string &base_ref,
595 const std::string &class_name_prefix);
615 return type.
get_bool(ID_C_java_generic_symbol);
653 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H std::vector< java_annotationt > & get_annotations()
The type of an expression.
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)
java_implicitly_generic_class_typet(const java_class_typet &class_type, const implicit_generic_typest &generic_types)
symbol_typet type_variablet
std::vector< symbol_exprt > java_lambda_method_handlest
bool is_reference_type(char t)
std::vector< valuet > & get_values()
optionalt< size_t > generic_type_index(const java_generic_parametert &type) const
Check if this symbol has the given generic type.
void add_lambda_method_handle(const irep_idt &identifier)
const java_lambda_method_handlest & lambda_method_handles() const
bool is_java_generic_symbol_type(const typet &type)
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
generic_typest & generic_types()
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 typet & java_generic_class_type_bound(size_t index, const typet &t)
Access information of the type bound of a generic java class type.
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...
std::string pretty_java_type(const typet &)
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.
java_generic_typet(const typet &_type)
void set_access(const irep_idt &access)
bool get_bool(const irep_namet &name) const
java_generic_class_typet()
java_generic_parametert(const irep_idt &_type_var_name, const symbol_typet &_bound)
bool is_valid_java_array(const struct_typet &)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
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 generic_type_argumentst & generic_type_arguments() const
const irep_idt & id() const
const java_generic_symbol_typet & to_java_generic_symbol_type(const typet &type)
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()
std::vector< reference_typet > generic_typest
const exprt & get_value() const
A reference into the symbol table.
implicit_generic_typest & implicit_generic_types()
const std::vector< java_annotationt > & get_annotations() const
typet java_array_element_type(const symbol_typet &array_type)
Return the type of the elements of a given java array type.
symbol_typet java_classname(const std::string &)
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 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 generic_typest & generic_types() const
Base class for tree-like data structures with sharing.
bool is_java_generic_class_type(const typet &type)
Type for a generic symbol, extends symbol_typet with a vector of java generic types.
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()
const implicit_generic_typest & implicit_generic_types() 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
const java_generic_typet & to_java_generic_type(const typet &type)
const type_variablest & type_variables() const
std::vector< type_variablet > type_variablest
type_variablest & type_variables()
std::string pretty_signature(const code_typet &)
Base class for all expressions.
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.
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>...
typet java_boolean_type()
const irep_idt get_name() const
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.
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.
generic_type_argumentst & generic_type_arguments()
const std::vector< valuet > & get_values() const
typet java_type_from_char(char t)
bool is_java_generic_type(const typet &type)
java_generic_symbol_typet(const symbol_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...
bool can_cast_type< annotated_typet >(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)
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)
const java_class_typet & to_java_class_type(const typet &type)
const irep_idt & get_identifier() const
const generic_typest & generic_types() const
std::vector< java_generic_parametert > generic_typest