Go to the documentation of this file.
8 #ifndef CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
9 #define CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
22 typedef std::unordered_map<irep_idt, std::vector<reference_typet>>
54 &generic_parameter_specialization_map,
91 &generic_parameter_specialization_map,
95 #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
std::set< irep_idt > generic_parameter_recursion_trackingt
virtual std::set< struct_tag_typet > get_parameter_alternative_types(const irep_idt &function_name, const irep_idt ¶meter_name, const namespacet &ns) const
Get alternative types for a method parameter, e.g., based on the casts in the function body.
virtual pointer_typet convert_pointer_type(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, const namespacet &ns) const
Select what type should be used for a given pointer type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
optionalt< pointer_typet > get_recursively_instantiated_type(const irep_idt &, const generic_parameter_specialization_mapt &, generic_parameter_recursion_trackingt &, const size_t) const
See get_recursively instantiated_type, the additional parameters just track the recursion to prevent ...
pointer_typet pointer_type(const typet &subtype)
nonstd::optional< T > optionalt
pointer_typet specialize_generics(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, generic_parameter_recursion_trackingt &visited_nodes) const
Specialize generic parameters in a pointer type based on the current map of parameters -> types.
virtual ~select_pointer_typet()=default
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...