cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
15
#include <set>
16
17
#include <
util/pointer_expr.h
>
18
19
class
generic_parameter_specialization_mapt
;
20
class
namespacet
;
21
22
class
select_pointer_typet
23
{
24
public
:
25
virtual
~select_pointer_typet
() =
default
;
26
36
virtual
pointer_typet
convert_pointer_type
(
37
const
pointer_typet
&
pointer_type
,
38
const
generic_parameter_specialization_mapt
39
&generic_parameter_specialization_map,
40
const
namespacet
&ns)
const
;
41
46
virtual
std::set<struct_tag_typet>
get_parameter_alternative_types
(
47
const
irep_idt
&function_name,
48
const
irep_idt
¶meter_name,
49
const
namespacet
&ns)
const
;
50
80
pointer_typet
specialize_generics
(
81
const
pointer_typet
&
pointer_type
,
82
const
generic_parameter_specialization_mapt
83
&generic_parameter_specialization_map)
const
;
84
};
85
86
#endif
// CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition
c_types.cpp:235
generic_parameter_specialization_mapt
Author: Diffblue Ltd.
Definition
generic_parameter_specialization_map.h:24
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition
pointer_expr.h:24
select_pointer_typet
Definition
select_pointer_type.h:23
select_pointer_typet::~select_pointer_typet
virtual ~select_pointer_typet()=default
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 ¶meter_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:84
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:30
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:20
pointer_expr.h
API to expression classes for Pointers.
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
jbmc
src
java_bytecode
select_pointer_type.h
Generated by
1.17.0