CBMC
generic_parameter_specialization_map_keys.h
Go to the documentation of this file.
1 
3 #ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
4 #define CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
5 
7 
15 {
16 private:
20  std::optional<std::size_t> container_id;
21 
22 public:
29  {
30  }
31 
35  {
36  if(container_id)
38  }
39 
40  // Objects of these class cannot be copied in any way - delete the copy
41  // constructor and copy assignment operator
46 
47  void insert(
49  const typet &pointer_subtype_struct);
50 
51  void insert(const struct_tag_typet &, const typet &symbol_struct);
52 };
53 
54 #endif // CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
std::optional< std::size_t > container_id
Key of the container to pop on destruction.
generic_parameter_specialization_map_keyst(const generic_parameter_specialization_map_keyst &)=delete
~generic_parameter_specialization_map_keyst()
Removes the top of the stack for each key in erase_keys from the controlled map.
generic_parameter_specialization_mapt & generic_parameter_specialization_map
Generic parameter specialization map to modify.
void insert(const pointer_typet &pointer_type, const typet &pointer_subtype_struct)
Author: Diffblue Ltd.
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.
generic_parameter_specialization_map_keyst & operator=(const generic_parameter_specialization_map_keyst &)=delete
void pop(std::size_t container_index)
Pop the top of the specialization stack for a given container.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:493
The type of an expression, extends irept.
Definition: type.h:29