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 
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
void propagate_const_function_pointers(symbol_tablet &symbol_tables, goto_functionst &goto_functions, message_handlert &message_handler)
The symbol table.
Definition: symbol_table.h:52