cprover
generic_parameter_specialization_map_keys.h
Go to the documentation of this file.
1 
3 
4 #ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
5 #define CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
6 
7 #include "select_pointer_type.h"
8 #include "java_types.h"
9 
17 {
18 public:
24  &_generic_parameter_specialization_map)
26  _generic_parameter_specialization_map)
27  {
28  }
29 
33  {
34  for(const auto key : erase_keys)
35  {
37  auto &val = generic_parameter_specialization_map.find(key)->second;
38  val.pop_back();
39  if(val.empty())
41  }
42  }
43 
44  // Objects of these class cannot be copied in any way - delete the copy
45  // constructor and copy assignment operator
50 
53  const typet &pointer_subtype_struct);
54  void
55  insert_pairs_for_symbol(const struct_tag_typet &, const typet &symbol_struct);
56 
57 private:
61  std::vector<irep_idt> erase_keys;
62 
63  void insert_pairs(
64  const std::vector<java_generic_parametert> &parameters,
65  const std::vector<reference_typet> &types);
66 };
67 
68 #endif // CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
The type of an expression, extends irept.
Definition: type.h:27
void insert_pairs(const std::vector< java_generic_parametert > &parameters, const std::vector< reference_typet > &types)
Add pairs to the controlled map.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
std::vector< irep_idt > erase_keys
Keys of the entries to pop on destruction.
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
void insert_pairs_for_symbol(const struct_tag_typet &, const typet &symbol_struct)
Add a pair of a parameter and its types for each generic parameter of the given generic symbol type t...
~generic_parameter_specialization_map_keyst()
Removes the top of the stack for each key in erase_keys from the controlled map.
The pointer type These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (they ...
Definition: std_types.h:1507
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 ...
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
generic_parameter_specialization_map_keyst & operator=(const generic_parameter_specialization_map_keyst &)=delete
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...
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
generic_parameter_specialization_mapt & generic_parameter_specialization_map
Generic parameter specialization map to modify.