CBMC
generic_parameter_specialization_map_keys.cpp
Go to the documentation of this file.
1 
4 
13  const typet &pointer_subtype_struct)
14 {
15  // Use a fresh generic_parameter_specialization_map_keyst for each scope
18  return;
19  // The supplied type must be the full type of the pointer's subtype
21  pointer_type.base_type().get(ID_identifier) ==
22  pointer_subtype_struct.get(ID_name));
23 
24  // If the pointer points to:
25  // - an incomplete class or
26  // - a class that is neither generic nor implicitly generic (this
27  // may be due to unsupported class signature)
28  // then ignore the generic types in the pointer and do not add an entry.
29  // TODO TG-1996 should decide how mocking and generics should work
30  // together. Currently an incomplete class is never marked as generic. If
31  // this changes in TG-1996 then the condition below should be updated.
32  if(to_java_class_type(pointer_subtype_struct).get_is_stub())
33  return;
34  if(
35  !is_java_generic_class_type(pointer_subtype_struct) &&
36  !is_java_implicitly_generic_class_type(pointer_subtype_struct))
37  {
38  return;
39  }
40 
41  const java_generic_typet &generic_pointer =
43 
44  const std::vector<java_generic_parametert> &generic_parameters =
45  get_all_generic_parameters(pointer_subtype_struct);
47  generic_pointer.generic_type_arguments();
48  INVARIANT(
49  type_args.size() == generic_parameters.size(),
50  "All generic parameters of the pointer type need to be specified");
51 
52  container_id =
53  generic_parameter_specialization_map.insert(generic_parameters, type_args);
54 }
55 
66  const struct_tag_typet &struct_tag_type,
67  const typet &symbol_struct)
68 {
69  // Use a fresh generic_parameter_specialization_map_keyst for each scope
71  if(!is_java_generic_struct_tag_type(struct_tag_type))
72  return;
73  // The supplied type must be the full type of the pointer's subtype
75  struct_tag_type.get(ID_identifier) == symbol_struct.get(ID_name));
76 
77  // If the struct is:
78  // - an incomplete class or
79  // - a class that is neither generic nor implicitly generic (this
80  // may be due to unsupported class signature)
81  // then ignore the generic types in the struct and do not add an entry.
82  // TODO TG-1996 should decide how mocking and generics should work
83  // together. Currently an incomplete class is never marked as generic. If
84  // this changes in TG-1996 then the condition below should be updated.
85  if(to_java_class_type(symbol_struct).get_is_stub())
86  return;
87  if(
88  !is_java_generic_class_type(symbol_struct) &&
90  {
91  return;
92  }
93 
94  const java_generic_struct_tag_typet &generic_symbol =
95  to_java_generic_struct_tag_type(struct_tag_type);
96 
97  const std::vector<java_generic_parametert> &generic_parameters =
98  get_all_generic_parameters(symbol_struct);
100  generic_symbol.generic_types();
101  INVARIANT(
102  type_args.size() == generic_parameters.size(),
103  "All generic parameters of the superclass need to be concretized");
104 
105  container_id =
106  generic_parameter_specialization_map.insert(generic_parameters, type_args);
107 }
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_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.
std::size_t insert(const std::vector< java_generic_parametert > &parameters, std::vector< reference_typet > types)
Insert a specialization for each type parameters of a container.
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:857
const generic_typest & generic_types() const
Definition: java_types.h:872
Reference that points to a java_generic_struct_tag_typet.
Definition: java_types.h:914
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:925
java_generic_struct_tag_typet::generic_typest generic_type_argumentst
Definition: java_types.h:916
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
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
std::vector< java_generic_parametert > get_all_generic_parameters(const typet &type)
Definition: java_types.cpp:924
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:581
bool is_java_generic_type(const typet &type)
Definition: java_types.h:946
bool is_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:888
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:994
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:1099
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:953
const java_generic_struct_tag_typet & to_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:896
#define PRECONDITION(CONDITION)
Definition: invariant.h:463