CBMC
Loading...
Searching...
No Matches
rebuild_goto_start_function.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Programs
4
5Author: Thomas Kiley, thomas@diffblue.com
6
7\*******************************************************************/
8
11
13
14#include <util/prefix.h>
16
18
19#include <langapi/language.h>
20#include <langapi/mode.h>
21
22#include <memory>
23
24std::unique_ptr<languaget> get_entry_point_language(
25 const symbol_table_baset &symbol_table,
26 const optionst &options,
27 message_handlert &message_handler)
28{
29 const irep_idt &mode = get_entry_point_mode(symbol_table);
30
31 // Get the relevant languaget to generate the new entry point with.
32 std::unique_ptr<languaget> language = get_language_from_mode(mode);
33 // This might fail if the driver program hasn't registered that language.
34 INVARIANT(language, "No language found for mode: " + id2string(mode));
35 language->set_language_options(options, message_handler);
36 return language;
37}
38
40{
43 return current_entry_point.mode;
44}
45
47{
48 // Remove the function itself
50
51 // And any symbols created in the scope of the entry point
52 std::vector<irep_idt> entry_point_symbols;
53 for(const auto &symbol_entry : symbol_table.symbols)
54 {
55 const bool is_entry_point_symbol=
59
61 entry_point_symbols.push_back(symbol_entry.first);
62 }
63
65 {
66 symbol_table.remove(entry_point_symbol);
67 }
68}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
The symbol table base class interface.
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Abstract interface to support a programming language.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition mode.cpp:51
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...
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.
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.
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Author: Diffblue Ltd.