cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
splice_call.cpp
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
15
16
#include "
splice_call.h
"
17
18
#include <
util/message.h
>
19
#include <
util/namespace.h
>
20
#include <
util/string_utils.h
>
21
#include <
util/symbol.h
>
22
23
#include <
goto-programs/goto_functions.h
>
24
25
// split the argument in caller/ callee two-position vector
26
// expect input as a string of two names glued with comma: "caller,callee"
27
static
bool
parse_caller_callee
(
28
const
std::string &callercallee,
29
std::vector<std::string> &result)
30
{
31
result =
split_string
(callercallee,
','
);
32
return
result.size() != 2;
33
}
34
35
bool
splice_call
(
36
goto_functionst
&goto_functions,
37
const
std::string &callercallee,
38
const
symbol_table_baset
&symbol_table,
39
message_handlert
&message_handler)
40
{
41
messaget
message(message_handler);
42
const
namespacet
ns(symbol_table);
43
std::vector<std::string> caller_callee;
44
if
(
parse_caller_callee
(callercallee, caller_callee))
45
{
46
message.
error
() <<
"Expecting two function names separated by a comma"
47
<<
messaget::eom
;
48
return
true
;
49
}
50
goto_functionst::function_mapt::iterator caller_fun=
51
goto_functions.
function_map
.find(caller_callee[0]);
52
goto_functionst::function_mapt::const_iterator callee_fun=
53
goto_functions.
function_map
.find(caller_callee[1]);
54
if
(caller_fun==goto_functions.
function_map
.end())
55
{
56
message.
error
() <<
"Caller function does not exist"
<<
messaget::eom
;
57
return
true
;
58
}
59
if
(!caller_fun->second.body_available())
60
{
61
message.
error
() <<
"Caller function has no available body"
<<
messaget::eom
;
62
return
true
;
63
}
64
if
(callee_fun==goto_functions.
function_map
.end())
65
{
66
message.
error
() <<
"Callee function does not exist"
<<
messaget::eom
;
67
return
true
;
68
}
69
goto_programt::const_targett
start=
70
caller_fun->second.body.instructions.begin();
71
const
code_function_callt
splice_call
(
72
ns.
lookup
(callee_fun->first).symbol_expr());
73
caller_fun->second.body.insert_before(
74
start,
goto_programt::make_function_call
(
splice_call
));
75
76
// update counters etc.
77
goto_functions.
update
();
78
return
false
;
79
}
code_function_callt
goto_instruction_codet representation of a function call statement.
Definition
goto_instruction_code.h:271
goto_functionst
A collection of goto functions.
Definition
goto_functions.h:25
goto_functionst::function_map
function_mapt function_map
Definition
goto_functions.h:29
goto_functionst::update
void update()
Definition
goto_functions.h:88
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition
goto_program.h:614
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition
goto_program.h:1089
message_handlert
Definition
message.h:27
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition
message.h:154
messaget::error
mstreamt & error() const
Definition
message.h:391
messaget::eom
static eomt eom
Definition
message.h:289
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition
namespace.cpp:134
symbol_table_baset
The symbol table base class interface.
Definition
symbol_table_base.h:23
goto_functions.h
Goto Programs with Functions.
namespace.h
parse_caller_callee
static bool parse_caller_callee(const std::string &callercallee, std::vector< std::string > &result)
Definition
splice_call.cpp:27
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
splice_call.h
Harnessing for goto functions.
message.h
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition
string_utils.cpp:39
string_utils.h
symbol.h
Symbol table entry.
goto-instrument
splice_call.cpp
Generated by
1.17.0