cprover
remove_const_function_pointers.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Programs
4 
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H
13 #define CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H
14 
15 #include <unordered_set>
16 
17 #include "goto_model.h"
18 #include <util/message.h>
19 #include <util/expr.h>
20 #include <util/namespace.h>
21 
22 
24 {
25 public:
26  typedef std::unordered_set<exprt, irep_hash> functionst;
27  typedef std::list<exprt> expressionst;
30  const namespacet &ns,
32 
33  bool operator()(const exprt &base_expression, functionst &out_functions);
34 
35 private:
36  exprt replace_const_symbols(const exprt &expression) const;
37  exprt resolve_symbol(const symbol_exprt &symbol_expr) const;
38 
39  // recursive functions for dealing with the function pointer
40  bool try_resolve_function_call(const exprt &expr, functionst &out_functions);
41 
43  const expressionst &exprs, functionst &out_functions);
44 
46  const index_exprt &index_expr, functionst &out_functions);
47 
49  const member_exprt &member_expr, functionst &out_functions);
50 
52  const address_of_exprt &address_expr, functionst &out_functions);
53 
55  const dereference_exprt &deref_expr, functionst &out_functions);
56 
58  const typecast_exprt &typecast_expr, functionst &out_functions);
59 
60  // recursive functions for dealing with the auxiliary elements
62  const exprt &expr,
63  expressionst &out_resolved_expression,
64  bool &out_is_const);
65 
67  const index_exprt &index_expr,
68  expressionst &out_expressions,
69  bool &out_is_const);
70 
71  bool try_resolve_member(
72  const member_exprt &member_expr,
73  expressionst &out_expressions,
74  bool &out_is_const);
75 
77  const dereference_exprt &deref_expr,
78  expressionst &out_expressions,
79  bool &out_is_const);
80 
82  const typecast_exprt &typecast_expr,
83  expressionst &out_expressions,
84  bool &out_is_const);
85 
86  bool is_const_expression(const exprt &expression) const;
87  bool is_const_type(const typet &type) const;
88 
90  const exprt &index_value_expr, mp_integer &out_array_index);
91 
93  const struct_exprt &struct_expr, const member_exprt &member_expr);
94 
95  const namespacet &ns;
97 };
98 
99 #define OPT_REMOVE_CONST_FUNCTION_POINTERS \
100  "(remove-const-function-pointers)"
101 
102 #define HELP_REMOVE_CONST_FUNCTION_POINTERS \
103  " --remove-const-function-pointers Remove function pointers that are constant or constant part of an array\n" // NOLINT(*)
104 
105 
106 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H
exprt replace_const_symbols(const exprt &expression) const
To collapse the symbols down to their values where possible This takes a very general approach...
The type of an expression.
Definition: type.h:20
semantic type conversion
Definition: std_expr.h:1725
remove_const_function_pointerst(message_handlert &message_handler, const namespacet &ns, const symbol_tablet &symbol_table)
To take a function call on a function pointer, and if possible resolve it to a small collection of po...
BigInt mp_integer
Definition: mp_arith.h:19
bool try_resolve_typecast_function_call(const typecast_exprt &typecast_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
exprt get_component_value(const struct_exprt &struct_expr, const member_exprt &member_expr)
To extract the value of the specific component within a struct.
bool try_resolve_member_function_call(const member_exprt &member_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
bool try_resolve_index_of(const index_exprt &index_expr, expressionst &out_expressions, bool &out_is_const)
To squash an index access by first finding the array it is accessing Then if the index can be resolve...
bool try_resolve_typecast(const typecast_exprt &typecast_expr, expressionst &out_expressions, bool &out_is_const)
To squash a typecast access.
bool try_resolve_dereference(const dereference_exprt &deref_expr, expressionst &out_expressions, bool &out_is_const)
To squash a dereference access by first finding the address_of the dereference is dereferencing...
std::unordered_set< exprt, irep_hash > functionst
Extract member of struct or union.
Definition: std_expr.h:3214
bool try_resolve_function_calls(const expressionst &exprs, functionst &out_functions)
To resolve a collection of expressions to the specific function calls they can be.
Symbol Table + CFG.
bool try_resolve_member(const member_exprt &member_expr, expressionst &out_expressions, bool &out_is_const)
To squash an member access by first finding the struct it is accessing Then return the squashed value...
bool try_resolve_expression(const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
To squash various expr types to simplify the expression.
exprt resolve_symbol(const symbol_exprt &symbol_expr) const
Look up a symbol in the symbol table and return its value.
bool is_const_expression(const exprt &expression) const
To evaluate the const-ness of the expression type.
bool try_resolve_index_value(const exprt &index_value_expr, mp_integer &out_array_index)
Given an index into an array, resolve, if possible, the index that is being accessed.
Operator to dereference a pointer.
Definition: std_expr.h:2701
The symbol table.
Definition: symbol_table.h:52
bool try_resolve_index_of_function_call(const index_exprt &index_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool operator()(const exprt &base_expression, functionst &out_functions)
To take a function call on a function pointer, and if possible resolve it to a small collection of po...
Operator to return the address of an object.
Definition: std_expr.h:2593
bool try_resolve_dereference_function_call(const dereference_exprt &deref_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
bool try_resolve_address_of_function_call(const address_of_exprt &address_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
Base class for all expressions.
Definition: expr.h:46
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool try_resolve_function_call(const exprt &expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
struct constructor from list of elements
Definition: std_expr.h:1464
message_handlert * message_handler
Definition: message.h:259
bool is_const_type(const typet &type) const
To evaluate the const-ness of the type.
array index operator
Definition: std_expr.h:1170