-
Notifications
You must be signed in to change notification settings - Fork 273
/
Copy pathremove_const_function_pointers.h
116 lines (86 loc) · 3.5 KB
/
remove_const_function_pointers.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
/*******************************************************************\
Module: Goto Programs
Author: Thomas Kiley, [email protected]
\*******************************************************************/
/// \file
/// Goto Programs
#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H
#define CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H
#include <list>
#include <unordered_set>
#include <util/expr.h>
#include <util/message.h>
#include <util/mp_arith.h>
class address_of_exprt;
class dereference_exprt;
class index_exprt; // IWYU pragma: keep
class member_exprt; // IWYU pragma: keep
class namespacet;
class struct_exprt; // IWYU pragma: keep
class symbol_exprt; // IWYU pragma: keep
class symbol_table_baset;
class typecast_exprt; // IWYU pragma: keep
class remove_const_function_pointerst
{
public:
typedef std::unordered_set<symbol_exprt, irep_hash> functionst;
typedef std::list<exprt> expressionst;
remove_const_function_pointerst(
message_handlert &message_handler,
const namespacet &ns,
const symbol_table_baset &symbol_table);
bool operator()(const exprt &base_expression, functionst &out_functions);
private:
exprt replace_const_symbols(const exprt &expression) const;
exprt resolve_symbol(const symbol_exprt &symbol_expr) const;
// recursive functions for dealing with the function pointer
bool try_resolve_function_call(const exprt &expr, functionst &out_functions);
bool try_resolve_function_calls(
const expressionst &exprs, functionst &out_functions);
bool try_resolve_index_of_function_call(
const index_exprt &index_expr, functionst &out_functions);
bool try_resolve_member_function_call(
const member_exprt &member_expr, functionst &out_functions);
bool try_resolve_address_of_function_call(
const address_of_exprt &address_expr, functionst &out_functions);
bool try_resolve_dereference_function_call(
const dereference_exprt &deref_expr, functionst &out_functions);
bool try_resolve_typecast_function_call(
const typecast_exprt &typecast_expr, functionst &out_functions);
// recursive functions for dealing with the auxiliary elements
bool try_resolve_expression(
const exprt &expr,
expressionst &out_resolved_expression,
bool &out_is_const);
bool try_resolve_index_of(
const index_exprt &index_expr,
expressionst &out_expressions,
bool &out_is_const);
bool try_resolve_member(
const member_exprt &member_expr,
expressionst &out_expressions,
bool &out_is_const);
bool try_resolve_dereference(
const dereference_exprt &deref_expr,
expressionst &out_expressions,
bool &out_is_const);
bool try_resolve_typecast(
const typecast_exprt &typecast_expr,
expressionst &out_expressions,
bool &out_is_const);
bool is_const_expression(const exprt &expression) const;
bool is_const_type(const typet &type) const;
bool try_resolve_index_value(
const exprt &index_value_expr, mp_integer &out_array_index);
exprt get_component_value(
const struct_exprt &struct_expr, const member_exprt &member_expr);
messaget log;
const namespacet &ns;
const symbol_table_baset &symbol_table;
};
#define OPT_REMOVE_CONST_FUNCTION_POINTERS \
"(remove-const-function-pointers)"
#define HELP_REMOVE_CONST_FUNCTION_POINTERS \
" {y--remove-const-function-pointers} \t " \
"remove function pointers that are constant or constant part of an array\n"
#endif // CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H