cprover
rebuild_goto_start_function.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2  Module: Goto Programs
3  Author: Thomas Kiley, thomas@diffblue.com
4 \*******************************************************************/
5 
8 
10 
11 #include <util/symbol.h>
12 #include <util/symbol_table.h>
13 #include <util/prefix.h>
14 #include <util/cmdline.h>
15 
16 #include <langapi/mode.h>
17 #include <langapi/language.h>
18 
19 #include <memory>
20 
27 template<typename maybe_lazy_goto_modelt>
30  const cmdlinet &cmdline,
31  maybe_lazy_goto_modelt &goto_model,
34  cmdline(cmdline),
35  goto_model(goto_model)
36 {
37 }
38 
47 template<typename maybe_lazy_goto_modelt>
49 {
50  const irep_idt &mode=get_entry_point_mode();
51 
52  // Get the relevant languaget to generate the new entry point with
53  std::unique_ptr<languaget> language=get_language_from_mode(mode);
54  INVARIANT(language, "No language found for mode: "+id2string(mode));
55  language->set_message_handler(get_message_handler());
56  language->get_language_options(cmdline);
57 
58  // To create a new entry point we must first remove the old one
59  remove_existing_entry_point();
60 
61  bool return_code=
62  language->generate_support_functions(goto_model.symbol_table);
63 
64  // Remove the function from the goto functions so it is copied back in
65  // from the symbol table during goto_convert
66  if(!return_code)
67  goto_model.unload(goto_functionst::entry_point());
68 
69  return return_code;
70 }
71 
75 template<typename maybe_lazy_goto_modelt>
78 {
79  const symbolt &current_entry_point=
80  *goto_model.symbol_table.lookup(goto_functionst::entry_point());
81  return current_entry_point.mode;
82 }
83 
86 template<typename maybe_lazy_goto_modelt>
89 {
90  // Remove the function itself
91  goto_model.symbol_table.remove(goto_functionst::entry_point());
92 
93  // And any symbols created in the scope of the entry point
94  std::vector<irep_idt> entry_point_symbols;
95  for(const auto &symbol_entry : goto_model.symbol_table.symbols)
96  {
97  const bool is_entry_point_symbol=
98  has_prefix(
99  id2string(symbol_entry.first),
101 
102  if(is_entry_point_symbol)
103  entry_point_symbols.push_back(symbol_entry.first);
104  }
105 
106  for(const irep_idt &entry_point_symbol : entry_point_symbols)
107  {
108  goto_model.symbol_table.remove(entry_point_symbol);
109  }
110 }
111 
rebuild_goto_start_function_baset(const cmdlinet &cmdline, maybe_lazy_goto_modelt &goto_model, message_handlert &message_handler)
To rebuild the _start function in the event the program was compiled into GOTO with a different entry...
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Symbol table entry.
irep_idt mode
Language mode.
Definition: symbol.h:52
virtual void get_language_options(const cmdlinet &)
Definition: language.h:43
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
irep_idt get_entry_point_mode() const
Find out the mode of the current entry point to determine the mode of the replacement entry point...
Abstract interface to support a programming language.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
bool operator()()
To rebuild the _start function in the event the program was compiled into GOTO with a different entry...
static irep_idt entry_point()
void remove_existing_entry_point()
Eliminate the existing entry point function symbol and any symbols created in that scope from the sym...
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66