cprover
generic_parameter_specialization_map_keyst Class Reference

#include <generic_parameter_specialization_map_keys.h>

Collaboration diagram for generic_parameter_specialization_map_keyst:
[legend]

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_keystoperator= (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 > &parameters, const std::vector< reference_typet > &types)
 Add pairs to the controlled map. More...
 

Private Attributes

generic_parameter_specialization_maptgeneric_parameter_specialization_map
 Generic parameter specialization map to modify. More...
 
std::vector< irep_idterase_keys
 Keys of the entries to pop on destruction. More...
 

Detailed Description

Definition at line 15 of file generic_parameter_specialization_map_keys.h.

Constructor & Destructor Documentation

◆ generic_parameter_specialization_map_keyst() [1/2]

generic_parameter_specialization_map_keyst::generic_parameter_specialization_map_keyst ( generic_parameter_specialization_mapt _generic_parameter_specialization_map)
inlineexplicit

Initialize a generic-parameter-specialization-map entry owner operating on a given map.

Initially it does not own any map entry.

Parameters
_generic_parameter_specialization_mapmap to operate on.

Definition at line 21 of file generic_parameter_specialization_map_keys.h.

◆ ~generic_parameter_specialization_map_keyst()

generic_parameter_specialization_map_keyst::~generic_parameter_specialization_map_keyst ( )
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.

◆ generic_parameter_specialization_map_keyst() [2/2]

generic_parameter_specialization_map_keyst::generic_parameter_specialization_map_keyst ( const generic_parameter_specialization_map_keyst )
delete

Member Function Documentation

◆ insert_pairs()

const void generic_parameter_specialization_map_keyst::insert_pairs ( const std::vector< java_generic_parametert > &  parameters,
const std::vector< reference_typet > &  types 
)
private

Add pairs to the controlled map.

Own the keys and pop from their stack on destruction; otherwise do nothing.

Parameters
parametersgeneric parameters that are the keys of the pairs to add
typesa 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().

◆ insert_pairs_for_pointer()

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.

Parameters
pointer_typepointer type to get the specialized generic types from
pointer_subtype_structstruct 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().

◆ insert_pairs_for_symbol()

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.

Parameters
symbol_typesymbol type to get the specialized generic types from
symbol_structstruct 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().

◆ operator=()

generic_parameter_specialization_map_keyst& generic_parameter_specialization_map_keyst::operator= ( const generic_parameter_specialization_map_keyst )
delete

Member Data Documentation

◆ erase_keys

std::vector<irep_idt> generic_parameter_specialization_map_keyst::erase_keys
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().

◆ generic_parameter_specialization_map

generic_parameter_specialization_mapt& generic_parameter_specialization_map_keyst::generic_parameter_specialization_map
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().


The documentation for this class was generated from the following files: