cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
generic_parameter_specialization_map_keys.cpp
Go to the documentation of this file.
1
2
3
#include "
generic_parameter_specialization_map_keys.h
"
4
11
void
generic_parameter_specialization_map_keyst::insert
(
12
const
pointer_typet
&
pointer_type
,
13
const
typet
&pointer_subtype_struct)
14
{
15
// Use a fresh generic_parameter_specialization_map_keyst for each scope
16
PRECONDITION
(!
container_id
);
17
if
(!
is_java_generic_type
(
pointer_type
))
18
return
;
19
// The supplied type must be the full type of the pointer's subtype
20
PRECONDITION
(
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 =
42
to_java_generic_type
(
pointer_type
);
43
44
const
std::vector<java_generic_parametert> &generic_parameters =
45
get_all_generic_parameters
(pointer_subtype_struct);
46
const
java_generic_typet::generic_type_argumentst
&type_args =
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
65
void
generic_parameter_specialization_map_keyst::insert
(
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
70
PRECONDITION
(!
container_id
);
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
74
PRECONDITION
(
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) &&
89
!
is_java_implicitly_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);
99
const
java_generic_typet::generic_type_argumentst
&type_args =
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_type
pointer_typet pointer_type(const typet &subtype)
Definition
c_types.cpp:235
generic_parameter_specialization_map_keyst::container_id
std::optional< std::size_t > container_id
Key of the container to pop on destruction.
Definition
generic_parameter_specialization_map_keys.h:20
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:18
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:11
irept::get
const irep_idt & get(const irep_idt &name) const
Definition
irep.cpp:44
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:857
java_generic_struct_tag_typet::generic_types
const generic_typest & generic_types() const
Definition
java_types.h:872
java_generic_typet
Reference that points to a java_generic_struct_tag_typet.
Definition
java_types.h:914
java_generic_typet::generic_type_arguments
const generic_type_argumentst & generic_type_arguments() const
Definition
java_types.h:925
java_generic_typet::generic_type_argumentst
java_generic_struct_tag_typet::generic_typest generic_type_argumentst
Definition
java_types.h:916
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition
pointer_expr.h:24
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition
std_types.h:493
typet
The type of an expression, extends irept.
Definition
type.h:29
generic_parameter_specialization_map_keys.h
Author: Diffblue Ltd.
get_all_generic_parameters
std::vector< java_generic_parametert > get_all_generic_parameters(const typet &type)
Definition
java_types.cpp:924
to_java_generic_type
const java_generic_typet & to_java_generic_type(const typet &type)
Definition
java_types.h:953
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:896
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition
java_types.h:581
is_java_generic_type
bool is_java_generic_type(const typet &type)
Definition
java_types.h:946
is_java_generic_struct_tag_type
bool is_java_generic_struct_tag_type(const typet &type)
Definition
java_types.h:888
is_java_generic_class_type
bool is_java_generic_class_type(const typet &type)
Definition
java_types.h:994
is_java_implicitly_generic_class_type
bool is_java_implicitly_generic_class_type(const typet &type)
Definition
java_types.h:1099
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition
invariant.h:423
jbmc
src
java_bytecode
generic_parameter_specialization_map_keys.cpp
Generated by
1.17.0