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 
15 #include "java_types.h"
16 
17 #include <vector>
18 
19 #include "java_types.h"
20 #include <util/optional.h>
21 #include <util/std_types.h>
22 
23 class namespacet;
24 
26 {
27 public:
28  virtual ~select_pointer_typet() = default;
29 
42  &generic_parameter_specialization_map,
43  const namespacet &ns) const;
44 
49  virtual std::set<struct_tag_typet> get_parameter_alternative_types(
50  const irep_idt &function_name,
51  const irep_idt &parameter_name,
52  const namespacet &ns) const;
53 
86  &generic_parameter_specialization_map) const;
87 };
88 
89 #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
optional.h
select_pointer_typet::get_parameter_alternative_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.
Definition: select_pointer_type.cpp:81
generic_parameter_specialization_mapt
Author: Diffblue Ltd.
Definition: generic_parameter_specialization_map.h:24
select_pointer_typet::convert_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.
Definition: select_pointer_type.cpp:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
std_types.h
Pre-defined types.
select_pointer_typet
Definition: select_pointer_type.h:26
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
select_pointer_typet::~select_pointer_typet
virtual ~select_pointer_typet()=default
select_pointer_typet::specialize_generics
pointer_typet specialize_generics(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map) const
Specialize generic parameters in a pointer type based on the current map of parameters -> types.
Definition: select_pointer_type.cpp:27
java_types.h
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
generic_parameter_specialization_map.h