cprover
select_pointer_type.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Java Bytecode Language Conversion
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 #ifndef CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
9 #define CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
10 
14 #include "java_types.h"
15 
16 #include <vector>
17 
18 #include "java_types.h"
19 #include <util/optional.h>
20 #include <util/std_types.h>
21 
22 typedef std::unordered_map<irep_idt, std::vector<reference_typet>>
24 typedef std::set<irep_idt> generic_parameter_recursion_trackingt;
25 
26 class namespacet;
27 
29 {
31  const irep_idt &,
34  const size_t) const;
36  const irep_idt &parameter_name,
37  const generic_parameter_specialization_mapt &visited) const;
38 
39 public:
40  virtual ~select_pointer_typet() = default;
41 
54  &generic_parameter_specialization_map,
55  const namespacet &ns) const;
56 
61  virtual std::set<struct_tag_typet> get_parameter_alternative_types(
62  const irep_idt &function_name,
63  const irep_idt &parameter_name,
64  const namespacet &ns) const;
65 
91  &generic_parameter_specialization_map,
92  generic_parameter_recursion_trackingt &visited_nodes) const;
93 };
94 
95 #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
std::set< irep_idt > generic_parameter_recursion_trackingt
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)
Definition: c_types.cpp:243
virtual ~select_pointer_typet()=default
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.
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
nonstd::optional< T > optionalt
Definition: optional.h:35
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
Pre-defined types.
virtual std::set< struct_tag_typet > get_parameter_alternative_types(const irep_idt &function_name, const irep_idt &parameter_name, const namespacet &ns) const
Get alternative types for a method parameter, e.g., based on the casts in the function body.
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.