CBMC
splice_call.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Prepend/ splice a 0-ary function call in the beginning of a function
4 e.g. for setting/ modelling the global environment
5 
6 Author: Konstantinos Pouliasis
7 
8 Date: July 2017
9 
10 \*******************************************************************/
11 
14 
15 #ifndef CPROVER_GOTO_INSTRUMENT_SPLICE_CALL_H
16 #define CPROVER_GOTO_INSTRUMENT_SPLICE_CALL_H
17 
18 #include <string>
19 
20 class goto_functionst;
21 class message_handlert;
22 class symbol_table_baset;
23 
24 bool splice_call(
25  goto_functionst &goto_functions,
26  const std::string &callercallee,
27  const symbol_table_baset &symbol_table,
28  message_handlert &message_handler);
29 
30 #endif // CPROVER_GOTO_INSTRUMENT_SPLICE_CALL_H
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
message_handlert
Definition: message.h:27
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:23
splice_call
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_table_baset &symbol_table, message_handlert &message_handler)
Definition: splice_call.cpp:35