cprover
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 <
goto-programs/goto_functions.h
>
19
class
message_handlert
;
20
21
bool
splice_call
(
22
goto_functionst
&goto_functions,
23
const
std::string &callercallee,
24
const
symbol_tablet
&symbol_table,
25
message_handlert
&message_handler);
26
27
#endif // CPROVER_GOTO_INSTRUMENT_SPLICE_CALL_H
symbol_tablet
The symbol table.
Definition:
symbol_table.h:20
message_handlert
Definition:
message.h:28
splice_call
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_tablet &symbol_table, message_handlert &message_handler)
Definition:
splice_call.cpp:38
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:23
goto_functions.h
Goto Programs with Functions.
goto-instrument
splice_call.h
Generated by
1.8.20