Go to the documentation of this file.
20 &generic_parameter_specialization_map,
26 if(!generic_parameter_specialization_map.empty())
30 pointer_type, generic_parameter_specialization_map, visited);
31 INVARIANT(visited.empty(),
"recursion stack must be empty here");
43 &generic_parameter_specialization_map,
54 if(visited_nodes.find(parameter_name) != visited_nodes.end())
57 parameter_name, generic_parameter_specialization_map);
58 return result.has_value() ? result.value() :
pointer_type;
61 if(generic_parameter_specialization_map.count(parameter_name) == 0)
70 generic_parameter_specialization_map.
find(parameter_name)->second.back();
77 visited_nodes.insert(parameter_name);
80 generic_parameter_specialization_map,
82 visited_nodes.erase(parameter_name);
92 if(array_element_type.
id() == ID_pointer)
96 generic_parameter_specialization_map,
100 replacement_array_type.
subtype().
set(ID_element_type, new_array_type);
101 return replacement_array_type;
131 &generic_parameter_specialization_map)
const
134 const size_t max_depth =
135 generic_parameter_specialization_map.find(parameter_name)->second.size();
137 irep_idt current_parameter = parameter_name;
138 for(
size_t depth = 0; depth < max_depth; depth++)
141 current_parameter, generic_parameter_specialization_map, visited, depth);
142 if(retval.has_value())
150 generic_parameter_specialization_map.find(current_parameter)
173 &generic_parameter_specialization_map,
175 const size_t depth)
const
177 const auto &val = generic_parameter_specialization_map.find(parameter_name);
179 val != generic_parameter_specialization_map.end(),
180 "generic parameter must be a key in map");
182 const auto &replacements = val->second;
185 depth < replacements.size(),
"cannot access elements outside stack");
188 if(visited.find(parameter_name) != visited.end())
193 const size_t index = (replacements.size() - 1) - depth;
194 const auto &type = replacements[index];
201 visited.insert(parameter_name);
204 generic_parameter_specialization_map,
207 visited.erase(parameter_name);
211 std::set<struct_tag_typet>
219 (void)parameter_name;
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const typet & subtype() const
The type of an expression, extends irept.
const typet & java_array_element_type(const struct_tag_typet &array_symbol)
Return a const reference to the element type of a given java array type.
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
std::set< irep_idt > generic_parameter_recursion_trackingt
const irept & find(const irep_namet &name) const
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>.
bool is_java_array_tag(const irep_idt &tag)
See above.
virtual std::set< struct_tag_typet > get_parameter_alternative_types(const irep_idt &function_name, const irep_idt ¶meter_name, const namespacet &ns) const
Get alternative types for a method parameter, e.g., based on the casts in the function body.
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
virtual pointer_typet convert_pointer_type(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, const namespacet &ns) const
Select what type should be used for a given pointer type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const irep_idt get_name() const
bool is_java_generic_parameter(const typet &type)
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>.
optionalt< pointer_typet > get_recursively_instantiated_type(const irep_idt &, const generic_parameter_specialization_mapt &, generic_parameter_recursion_trackingt &, const size_t) const
See get_recursively instantiated_type, the additional parameters just track the recursion to prevent ...
pointer_typet pointer_type(const typet &subtype)
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
nonstd::optional< T > optionalt
pointer_typet specialize_generics(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, generic_parameter_recursion_trackingt &visited_nodes) const
Specialize generic parameters in a pointer type based on the current map of parameters -> types.
const java_generic_parametert & to_java_generic_parameter(const typet &type)
void set(const irep_namet &name, const irep_idt &value)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
#define CHECK_RETURN(CONDITION)