cprover
generic_parameter_specialization_map_keys.cpp
Go to the documentation of this file.
1
2
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();
49 type_args.size() == generic_parameters.size(),
50 "All generic parameters of the pointer type need to be specified");
51
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
106 generic_parameter_specialization_map.insert(generic_parameters, type_args);
107}
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
optionalt< 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:45
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:858
const generic_typest & generic_types() const
Definition: java_types.h:873
Reference that points to a java_generic_struct_tag_typet.
Definition: java_types.h:915
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:926
java_generic_struct_tag_typet::generic_typest generic_type_argumentst
Definition: java_types.h:917
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:449
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:917
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:954
const java_generic_struct_tag_typet & to_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:897
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:582
bool is_java_generic_type(const typet &type)
Definition: java_types.h:947
bool is_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:889
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:995
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:1100
#define PRECONDITION(CONDITION)
Definition: invariant.h:463