cprover
generic_parameter_specialization_map_keys.cpp
Go to the documentation of this file.
1 
4 
5 #include <util/range.h>
6 
15  const typet &pointer_subtype_struct)
16 {
17  // Use a fresh generic_parameter_specialization_map_keyst for each scope
20  return;
21  // The supplied type must be the full type of the pointer's subtype
23  pointer_type.subtype().get(ID_identifier) ==
24  pointer_subtype_struct.get(ID_name));
25 
26  // If the pointer points to:
27  // - an incomplete class or
28  // - a class that is neither generic nor implicitly generic (this
29  // may be due to unsupported class signature)
30  // then ignore the generic types in the pointer and do not add an entry.
31  // TODO TG-1996 should decide how mocking and generics should work
32  // together. Currently an incomplete class is never marked as generic. If
33  // this changes in TG-1996 then the condition below should be updated.
34  if(to_java_class_type(pointer_subtype_struct).get_is_stub())
35  return;
36  if(
37  !is_java_generic_class_type(pointer_subtype_struct) &&
38  !is_java_implicitly_generic_class_type(pointer_subtype_struct))
39  {
40  return;
41  }
42 
43  const java_generic_typet &generic_pointer =
45 
46  const std::vector<java_generic_parametert> &generic_parameters =
47  get_all_generic_parameters(pointer_subtype_struct);
49  generic_pointer.generic_type_arguments();
50  INVARIANT(
51  type_args.size() == generic_parameters.size(),
52  "All generic parameters of the pointer type need to be specified");
53 
54  container_id =
55  generic_parameter_specialization_map.insert(generic_parameters, type_args);
56 }
57 
68  const struct_tag_typet &struct_tag_type,
69  const typet &symbol_struct)
70 {
71  // Use a fresh generic_parameter_specialization_map_keyst for each scope
73  if(!is_java_generic_struct_tag_type(struct_tag_type))
74  return;
75  // The supplied type must be the full type of the pointer's subtype
77  struct_tag_type.get(ID_identifier) == symbol_struct.get(ID_name));
78 
79  // If the struct is:
80  // - an incomplete class or
81  // - a class that is neither generic nor implicitly generic (this
82  // may be due to unsupported class signature)
83  // then ignore the generic types in the struct and do not add an entry.
84  // TODO TG-1996 should decide how mocking and generics should work
85  // together. Currently an incomplete class is never marked as generic. If
86  // this changes in TG-1996 then the condition below should be updated.
87  if(to_java_class_type(symbol_struct).get_is_stub())
88  return;
89  if(
90  !is_java_generic_class_type(symbol_struct) &&
92  {
93  return;
94  }
95 
96  const java_generic_struct_tag_typet &generic_symbol =
97  to_java_generic_struct_tag_type(struct_tag_type);
98 
99  const std::vector<java_generic_parametert> &generic_parameters =
100  get_all_generic_parameters(symbol_struct);
102  generic_symbol.generic_types();
103  INVARIANT(
104  type_args.size() == generic_parameters.size(),
105  "All generic parameters of the superclass need to be concretized");
106 
107  container_id =
108  generic_parameter_specialization_map.insert(generic_parameters, type_args);
109 }
is_java_generic_class_type
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:995
typet::subtype
const typet & subtype() const
Definition: type.h:47
generic_parameter_specialization_map_keyst::insert
void insert(const pointer_typet &pointer_type, const typet &pointer_subtype_struct)
Author: Diffblue Ltd.
Definition: generic_parameter_specialization_map_keys.cpp:13
java_generic_typet
Reference that points to a java_generic_struct_tag_typet.
Definition: java_types.h:916
typet
The type of an expression, extends irept.
Definition: type.h:29
generic_parameter_specialization_map_keys.h
Author: Diffblue Ltd.
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
is_java_implicitly_generic_class_type
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:1100
java_generic_typet::generic_type_argumentst
java_generic_struct_tag_typet::generic_typest generic_type_argumentst
Definition: java_types.h:918
java_generic_struct_tag_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:874
to_java_generic_struct_tag_type
const java_generic_struct_tag_typet & to_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:898
java_generic_typet::generic_type_arguments
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:927
generic_parameter_specialization_mapt::insert
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.
Definition: generic_parameter_specialization_map.cpp:5
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
is_java_generic_struct_tag_type
bool is_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:890
is_java_generic_type
bool is_java_generic_type(const typet &type)
Definition: java_types.h:947
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
generic_parameter_specialization_map_keyst::generic_parameter_specialization_map
generic_parameter_specialization_mapt & generic_parameter_specialization_map
Generic parameter specialization map to modify.
Definition: generic_parameter_specialization_map_keys.h:19
to_java_generic_type
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:954
get_all_generic_parameters
std::vector< java_generic_parametert > get_all_generic_parameters(const typet &type)
Definition: java_types.cpp:918
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
java_generic_struct_tag_typet
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:859
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
generic_parameter_specialization_map_keyst::container_id
optionalt< std::size_t > container_id
Key of the container to pop on destruction.
Definition: generic_parameter_specialization_map_keys.h:21
validation_modet::INVARIANT
@ INVARIANT