CBMC
Loading...
Searching...
No Matches
splice_call.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Prepend/ splice a 0-ary function call in the beginning of a function
4e.g. for setting/ modelling the global environment
5
6Author: Konstantinos Pouliasis
7
8Date: 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
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"
28 const std::string &callercallee,
29 std::vector<std::string> &result)
30{
31 result = split_string(callercallee, ',');
32 return result.size() != 2;
33}
34
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;
45 {
46 message.error() << "Expecting two function names separated by a comma"
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 }
70 caller_fun->second.body.instructions.begin();
72 ns.lookup(callee_fun->first).symbol_expr());
73 caller_fun->second.body.insert_before(
75
76 // update counters etc.
77 goto_functions.update();
78 return false;
79}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
goto_instruction_codet representation of a function call statement.
A collection of goto functions.
function_mapt function_map
instructionst::const_iterator const_targett
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The symbol table base class interface.
Goto Programs with Functions.
static bool parse_caller_callee(const std::string &callercallee, std::vector< std::string > &result)
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_table_baset &symbol_table, message_handlert &message_handler)
Harnessing for goto functions.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Symbol table entry.