CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
generic_parameter_specialization_map.cpp
Go to the documentation of this file.
1
2
4
6 const std::vector<java_generic_parametert> &parameters,
7 std::vector<reference_typet> types)
8{
9 PRECONDITION(!parameters.empty());
10 const auto first_param_it =
11 param_to_container.find(parameters.front().get_name());
12 std::size_t container_index;
14 {
15 container_index = container_to_specializations.size();
16 container_to_specializations.emplace_back();
17 std::size_t param_index = 0;
18 for(const java_generic_parametert &parameter : parameters)
19 {
20 const auto result = param_to_container.emplace(
21 parameter.get_name(), container_paramt{container_index, param_index++});
23 result.second, "Some type parameters are already mapped but not all");
24 }
25 }
26 else
27 {
28 container_index = first_param_it->second.container_index;
29 std::size_t param_index = 0;
30 for(const java_generic_parametert &parameter : parameters)
31 {
32 const auto param_it = param_to_container.find(parameter.get_name());
35 "Some type parameters are already mapped but not all");
37 param_it->second.container_index == container_index,
38 "Not all type parameters are assigned to same container");
40 param_it->second.param_index == param_index,
41 "Type parameters have been encountered in two different orders");
42 ++param_index;
43 }
44 }
45 container_to_specializations[container_index].push(std::move(types));
46 return container_index;
47}
48
49void generic_parameter_specialization_mapt::pop(std::size_t container_index)
50{
51 container_to_specializations.at(container_index).pop();
52}
53
54std::optional<reference_typet>
56{
58 if(types_it == param_to_container.end())
59 return {};
60 std::stack<std::vector<reference_typet>> &stack =
61 container_to_specializations.at(types_it->second.container_index);
62 if(stack.empty())
63 return {};
64 reference_typet result = stack.top().at(types_it->second.param_index);
65 stack.pop();
66 return result;
67}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
std::vector< std::stack< std::vector< reference_typet > > > container_to_specializations
The list of containers and, for each one, the stack of lists of specializations.
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.
std::unordered_map< irep_idt, container_paramt > param_to_container
A map from parameter names to container_paramt instances.
void pop(std::size_t container_index)
Pop the top of the specialization stack for a given container.
Reference that points to a java_generic_parameter_tagt.
Definition java_types.h:775
The reference type.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
The index of the container and the type parameter inside that container.