cprover
|
#include <generic_parameter_specialization_map_keys.h>
Public Member Functions | |
generic_parameter_specialization_map_keyst (generic_parameter_specialization_mapt &_generic_parameter_specialization_map) | |
Initialize a generic-parameter-specialization-map entry owner operating on a given map. More... | |
~generic_parameter_specialization_map_keyst () | |
Removes the top of the stack for each key in erase_keys from the controlled map. More... | |
generic_parameter_specialization_map_keyst (const generic_parameter_specialization_map_keyst &)=delete | |
generic_parameter_specialization_map_keyst & | operator= (const generic_parameter_specialization_map_keyst &)=delete |
const void | insert_pairs_for_pointer (const pointer_typet &pointer_type, const typet &pointer_subtype_struct) |
Add a pair of a parameter and its types for each generic parameter of the given generic pointer type to the controlled map. More... | |
const void | insert_pairs_for_symbol (const symbol_typet &symbol_type, const typet &symbol_struct) |
Add a pair of a parameter and its types for each generic parameter of the given generic symbol type to the controlled map. More... | |
Private Member Functions | |
const void | insert_pairs (const std::vector< java_generic_parametert > ¶meters, const std::vector< reference_typet > &types) |
Add pairs to the controlled map. More... | |
Private Attributes | |
generic_parameter_specialization_mapt & | generic_parameter_specialization_map |
Generic parameter specialization map to modify. More... | |
std::vector< irep_idt > | erase_keys |
Keys of the entries to pop on destruction. More... | |
Definition at line 15 of file generic_parameter_specialization_map_keys.h.
|
inlineexplicit |
Initialize a generic-parameter-specialization-map entry owner operating on a given map.
Initially it does not own any map entry.
_generic_parameter_specialization_map | map to operate on. |
Definition at line 21 of file generic_parameter_specialization_map_keys.h.
|
inline |
Removes the top of the stack for each key in erase_keys from the controlled map.
Definition at line 31 of file generic_parameter_specialization_map_keys.h.
References erase_keys, generic_parameter_specialization_map, and PRECONDITION.
|
delete |
|
private |
Add pairs to the controlled map.
Own the keys and pop from their stack on destruction; otherwise do nothing.
parameters | generic parameters that are the keys of the pairs to add |
types | a type to add for each parameter |
Definition at line 42 of file generic_parameter_specialization_map_keys.cpp.
References erase_keys, generic_parameter_specialization_map, java_generic_parametert::get_name(), INVARIANT, is_java_generic_parameter(), PRECONDITION, and to_java_generic_parameter().
Referenced by insert_pairs_for_pointer(), and insert_pairs_for_symbol().
const void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer | ( | const pointer_typet & | pointer_type, |
const typet & | pointer_subtype_struct | ||
) |
Add a pair of a parameter and its types for each generic parameter of the given generic pointer type to the controlled map.
Own the keys and pop from their stack on destruction; otherwise do nothing.
pointer_type | pointer type to get the specialized generic types from |
pointer_subtype_struct | struct type to which the generic pointer points, must be generic if the pointer is generic |
Definition at line 93 of file generic_parameter_specialization_map_keys.cpp.
References java_generic_typet::generic_type_arguments(), irept::get(), get_all_generic_parameters(), irept::get_bool(), insert_pairs(), INVARIANT, is_java_generic_class_type(), is_java_generic_type(), is_java_implicitly_generic_class_type(), pointer_type(), PRECONDITION, typet::subtype(), and to_java_generic_type().
Referenced by java_object_factoryt::gen_nondet_init(), and java_object_factoryt::gen_nondet_pointer_init().
const void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol | ( | const symbol_typet & | symbol_type, |
const typet & | symbol_struct | ||
) |
Add a pair of a parameter and its types for each generic parameter of the given generic symbol type to the controlled map.
This function is used for generic bases (superclass or interfaces) where the reference to it is in the form of a symbol rather than a pointer (as opposed to the function insert_pairs_for_pointer). Own the keys and pop from their stack on destruction; otherwise do nothing.
symbol_type | symbol type to get the specialized generic types from |
symbol_struct | struct type of the symbol type, must be generic if the symbol is generic |
Definition at line 142 of file generic_parameter_specialization_map_keys.cpp.
References java_generic_symbol_typet::generic_types(), get_all_generic_parameters(), irept::get_bool(), insert_pairs(), INVARIANT, is_java_generic_class_type(), is_java_generic_symbol_type(), is_java_implicitly_generic_class_type(), and to_java_generic_symbol_type().
Referenced by java_object_factoryt::gen_nondet_init().
|
delete |
|
private |
Keys of the entries to pop on destruction.
Definition at line 61 of file generic_parameter_specialization_map_keys.h.
Referenced by insert_pairs(), and ~generic_parameter_specialization_map_keyst().
|
private |
Generic parameter specialization map to modify.
Definition at line 59 of file generic_parameter_specialization_map_keys.h.
Referenced by insert_pairs(), and ~generic_parameter_specialization_map_keyst().