CBMC
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/string_utils.h>
20 #include <util/symbol_table.h>
21 
23 
24 // split the argument in caller/ callee two-position vector
25 // expect input as a string of two names glued with comma: "caller,callee"
26 static bool parse_caller_callee(
27  const std::string &callercallee,
28  std::vector<std::string> &result)
29 {
30  result = split_string(callercallee, ',');
31  return result.size() != 2;
32 }
33 
35  goto_functionst &goto_functions,
36  const std::string &callercallee,
37  const symbol_tablet &symbol_table,
38  message_handlert &message_handler)
39 {
40  messaget message(message_handler);
41  const namespacet ns(symbol_table);
42  std::vector<std::string> caller_callee;
43  if(parse_caller_callee(callercallee, caller_callee))
44  {
45  message.error() << "Expecting two function names separated by a comma"
46  << messaget::eom;
47  return true;
48  }
49  goto_functionst::function_mapt::iterator caller_fun=
50  goto_functions.function_map.find(caller_callee[0]);
51  goto_functionst::function_mapt::const_iterator callee_fun=
52  goto_functions.function_map.find(caller_callee[1]);
53  if(caller_fun==goto_functions.function_map.end())
54  {
55  message.error() << "Caller function does not exist" << messaget::eom;
56  return true;
57  }
58  if(!caller_fun->second.body_available())
59  {
60  message.error() << "Caller function has no available body" << messaget::eom;
61  return true;
62  }
63  if(callee_fun==goto_functions.function_map.end())
64  {
65  message.error() << "Callee function does not exist" << messaget::eom;
66  return true;
67  }
69  caller_fun->second.body.instructions.begin();
71  ns.lookup(callee_fun->first).symbol_expr());
72  caller_fun->second.body.insert_before(
74 
75  // update counters etc.
76  goto_functions.update();
77  return false;
78 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
symbol_tablet
The symbol table.
Definition: symbol_table.h:13
string_utils.h
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:34
messaget::eom
static eomt eom
Definition: message.h:297
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
splice_call.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
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:1081
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
code_function_callt
goto_instruction_codet representation of a function call statement.
Definition: goto_instruction_code.h:271
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
messaget::error
mstreamt & error() const
Definition: message.h:399
message_handlert
Definition: message.h:27
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24
goto_functionst::update
void update()
Definition: goto_functions.h:83
goto_functions.h
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:587
symbol_table.h
Author: Diffblue Ltd.
message.h
parse_caller_callee
static bool parse_caller_callee(const std::string &callercallee, std::vector< std::string > &result)
Definition: splice_call.cpp:26