cprover
propagate_const_function_pointers.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Constant Function Pointer Propagation
4
5
Author: Vincent Nimal
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_MUSKETEER_PROPAGATE_CONST_FUNCTION_POINTERS_H
13
#define CPROVER_MUSKETEER_PROPAGATE_CONST_FUNCTION_POINTERS_H
14
15
class
symbol_tablet
;
16
class
goto_functionst
;
17
class
message_handlert
;
18
19
/* Note that it only propagates from MAIN, following the CFG, without
20
resolving non-constant function pointers. This is of particular interest
21
when used in conjunction with goto_partial_inline, so that it explores
22
inlined functions accepting generic functions (pthread_create in
23
particular) in their context, preventing a huge overapproximation of a
24
functions-based exploration in remove_function_pointers. */
25
26
void
propagate_const_function_pointers
(
27
symbol_tablet
&symbol_tables,
28
goto_functionst
&goto_functions,
29
message_handlert
&message_handler);
30
31
#endif // CPROVER_MUSKETEER_PROPAGATE_CONST_FUNCTION_POINTERS_H
propagate_const_function_pointers
void propagate_const_function_pointers(symbol_tablet &symbol_tables, goto_functionst &goto_functions, message_handlert &message_handler)
Definition:
propagate_const_function_pointers.cpp:545
symbol_tablet
The symbol table.
Definition:
symbol_table.h:52
message_handlert
Definition:
message.h:20
goto_functionst
Definition:
goto_functions.h:20
musketeer
propagate_const_function_pointers.h
Generated by
1.8.14