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 std::set< irep_idt > generic_parameter_recursion_trackingt
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)
virtual ~select_pointer_typet()=default
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...
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
nonstd::optional< T > optionalt
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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.