cprover
|
#include <select_pointer_type.h>
Public Member Functions | |
virtual | ~select_pointer_typet ()=default |
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. More... | |
pointer_typet | specialize_generics (const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, generic_parameter_recursion_trackingt &visited) const |
Specialize generic parameters in a pointer type based on the current map of parameters -> types. More... | |
Private Member Functions | |
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 visiting the same depth again and specify which stack depth is analyzed. More... | |
optionalt< pointer_typet > | get_recursively_instantiated_type (const irep_idt ¶meter_name, const generic_parameter_specialization_mapt &visited) const |
Return the first concrete type instantiation if any such exists. More... | |
Definition at line 26 of file select_pointer_type.h.
|
virtualdefault |
|
virtual |
Select what type should be used for a given pointer type.
For the base class we just use the supplied type. Derived classes can override this behaviour to provide more sophisticated type selection. Generic parameters are replaced with their concrete type.
pointer_type | The pointer type replace |
generic_parameter_specialization_map | map of types for all generic parameters in the current scope |
Definition at line 25 of file select_pointer_type.cpp.
References INVARIANT, pointer_type(), and specialize_generics().
Referenced by ci_lazy_methods_neededt::add_all_needed_classes(), and java_object_factoryt::gen_nondet_pointer_init().
|
private |
See get_recursively instantiated_type, the additional parameters just track the recursion to prevent visiting the same depth again and specify which stack depth is analyzed.
parameter_name | The name of the generic parameter type we want to have instantiated |
generic_parameter_specialization_map | Map of type names to specialization stack |
visited | Tracks the visited parameter names |
depth | Stack depth to analyze |
Definition at line 185 of file select_pointer_type.cpp.
References INVARIANT, is_java_generic_parameter(), and to_java_generic_parameter().
Referenced by get_recursively_instantiated_type(), and specialize_generics().
|
private |
Return the first concrete type instantiation if any such exists.
This method is only to be called when the specialize_generics
cannot find an instantiation due to a loop in its recursion.
parameter_name | The name of the generic parameter type we want to have instantiated |
generic_parameter_specialization_map | Map of type names to specialization stack |
Definition at line 143 of file select_pointer_type.cpp.
References CHECK_RETURN, java_generic_parametert::get_name(), get_recursively_instantiated_type(), is_java_generic_parameter(), and to_java_generic_parameter().
pointer_typet select_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.
We specialize generics if the pointer is a java generic parameter or an array with generic parameters (java generic types are specialized recursively, their concrete types are already stored in the map and will be retrieved when needed e.g., to initialize fields). Example:
pointer_type | pointer to be specialized |
generic_parameter_specialization_map | map of types for all generic parameters in the current scope |
Definition at line 65 of file select_pointer_type.cpp.
References irept::find(), symbol_typet::get_identifier(), java_generic_parametert::get_name(), get_recursively_instantiated_type(), irept::id(), is_java_array_tag(), is_java_generic_parameter(), java_array_element_type(), java_array_type(), pointer_type(), irept::set(), typet::subtype(), to_java_generic_parameter(), to_pointer_type(), and to_symbol_type().
Referenced by convert_pointer_type().