Go to the documentation of this file.
44 const symbolt ¤t_entry_point =
46 return current_entry_point.
mode;
55 std::vector<irep_idt> entry_point_symbols;
56 for(
const auto &symbol_entry : symbol_table.
symbols)
58 const bool is_entry_point_symbol=
63 if(is_entry_point_symbol)
64 entry_point_symbols.push_back(symbol_entry.first);
67 for(
const irep_idt &entry_point_symbol : entry_point_symbols)
69 symbol_table.
remove(entry_point_symbol);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
virtual void set_language_options(const optionst &)
Set language-specific options.
irep_idt mode
Language mode.
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
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 std::string & id2string(const irep_idt &d)
The symbol table base class interface.
Abstract interface to support a programming language.
virtual void set_message_handler(message_handlert &_message_handler)
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.
Goto Programs with Functions.
bool has_prefix(const std::string &s, const std::string &prefix)
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.