cprover
rebuild_goto_start_function.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Programs
4 
5 Author: Thomas Kiley, thomas@diffblue.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/symbol.h>
15 #include <util/symbol_table.h>
16 #include <util/prefix.h>
17 #include <util/cmdline.h>
18 
19 #include <langapi/mode.h>
20 #include <langapi/language.h>
21 
23 
24 #include <memory>
25 
26 std::unique_ptr<languaget> get_entry_point_language(
27  const symbol_table_baset &symbol_table,
28  const optionst &options,
29  message_handlert &message_handler)
30 {
31  const irep_idt &mode = get_entry_point_mode(symbol_table);
32 
33  // Get the relevant languaget to generate the new entry point with.
34  std::unique_ptr<languaget> language = get_language_from_mode(mode);
35  // This might fail if the driver program hasn't registered that language.
36  INVARIANT(language, "No language found for mode: " + id2string(mode));
37  language->set_message_handler(message_handler);
38  language->set_language_options(options);
39  return language;
40 }
41 
43 {
44  const symbolt &current_entry_point =
46  return current_entry_point.mode;
47 }
48 
50 {
51  // Remove the function itself
52  symbol_table.remove(goto_functionst::entry_point());
53 
54  // And any symbols created in the scope of the entry point
55  std::vector<irep_idt> entry_point_symbols;
56  for(const auto &symbol_entry : symbol_table.symbols)
57  {
58  const bool is_entry_point_symbol=
59  has_prefix(
60  id2string(symbol_entry.first),
62 
63  if(is_entry_point_symbol)
64  entry_point_symbols.push_back(symbol_entry.first);
65  }
66 
67  for(const irep_idt &entry_point_symbol : entry_point_symbols)
68  {
69  symbol_table.remove(entry_point_symbol);
70  }
71 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
get_entry_point_mode
const irep_idt & get_entry_point_mode(const symbol_table_baset &symbol_table)
Find out the mode of the current entry point to determine the mode of the replacement entry point.
Definition: rebuild_goto_start_function.cpp:42
get_entry_point_language
std::unique_ptr< languaget > get_entry_point_language(const symbol_table_baset &symbol_table, const optionst &options, message_handlert &message_handler)
Find the language corresponding to the __CPROVER_start function.
Definition: rebuild_goto_start_function.cpp:26
optionst
Definition: options.h:23
prefix.h
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
mode.h
languaget::set_language_options
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:43
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
rebuild_goto_start_function.h
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
remove_existing_entry_point
void remove_existing_entry_point(symbol_table_baset &symbol_table)
Eliminate the existing entry point function symbol and any symbols created in that scope from the sym...
Definition: rebuild_goto_start_function.cpp:49
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
language.h
Abstract interface to support a programming language.
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
symbol.h
Symbol table entry.
message_handlert
Definition: message.h:28
symbol_table_baset::remove
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
Definition: symbol_table_base.cpp:27
cmdline.h
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
goto_functions.h
Goto Programs with Functions.
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
symbol_table.h
Author: Diffblue Ltd.
validation_modet::INVARIANT
@ INVARIANT