cprover
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 
14 // useful for context/ environment setting in arbitrary nodes
15 
16 #include "splice_call.h"
17 
18 #include <util/message.h>
19 #include <util/string2int.h>
20 #include <util/string_utils.h>
21 
22 #include <langapi/language.h>
23 
25 
26 #include <algorithm>
27 
28 // split the argument in caller/ callee two-position vector
29 // expect input as a string of two names glued with comma: "caller,callee"
30 static bool parse_caller_callee(
31  const std::string &callercallee,
32  std::vector<std::string> &result)
33 {
34  split_string(callercallee, ',', result);
35  return (result.size()!= 2);
36 }
37 
39  goto_functionst &goto_functions,
40  const std::string &callercallee,
41  const symbol_tablet &symbol_table,
42  message_handlert &message_handler)
43 {
44  messaget message(message_handler);
45  const namespacet ns(symbol_table);
46  std::vector<std::string> caller_callee;
47  if(parse_caller_callee(callercallee, caller_callee))
48  {
49  message.error() << "Expecting two function names separated by a comma"
50  << messaget::eom;
51  return true;
52  }
53  goto_functionst::function_mapt::iterator caller_fun=
54  goto_functions.function_map.find(caller_callee[0]);
55  goto_functionst::function_mapt::const_iterator callee_fun=
56  goto_functions.function_map.find(caller_callee[1]);
57  if(caller_fun==goto_functions.function_map.end())
58  {
59  message.error() << "Caller function does not exist" << messaget::eom;
60  return true;
61  }
62  if(!caller_fun->second.body_available())
63  {
64  message.error() << "Caller function has no available body" << messaget::eom;
65  return true;
66  }
67  if(callee_fun==goto_functions.function_map.end())
68  {
69  message.error() << "Callee function does not exist" << messaget::eom;
70  return true;
71  }
73  caller_fun->second.body.instructions.begin();
75  caller_fun->second.body.insert_before(start);
77  ns.lookup(callee_fun->first).symbol_expr());
78  g->make_function_call(splice_call);
79 
80  // update counters etc.
81  goto_functions.update();
82  return false;
83 }
Goto Programs with Functions.
function_mapt function_map
instructionst::iterator targett
Definition: goto_program.h:414
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:415
mstreamt & error() const
Definition: message.h:386
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Abstract interface to support a programming language.
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
static eomt eom
Definition: message.h:284
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Given a string s, split into a sequence of substrings when separated by specified delimiter...
Harnessing for goto functions.
static bool parse_caller_callee(const std::string &callercallee, std::vector< std::string > &result)
Definition: splice_call.cpp:30
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
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