27 template<
typename maybe_lazy_goto_modelt>
31 maybe_lazy_goto_modelt &goto_model,
35 goto_model(goto_model)
47 template<
typename maybe_lazy_goto_modelt>
50 const irep_idt &mode=get_entry_point_mode();
59 remove_existing_entry_point();
75 template<
typename maybe_lazy_goto_modelt>
79 const symbolt ¤t_entry_point=
81 return current_entry_point.
mode;
86 template<
typename maybe_lazy_goto_modelt>
94 std::vector<irep_idt> entry_point_symbols;
95 for(
const auto &symbol_entry : goto_model.symbol_table.symbols)
97 const bool is_entry_point_symbol=
102 if(is_entry_point_symbol)
103 entry_point_symbols.push_back(symbol_entry.first);
106 for(
const irep_idt &entry_point_symbol : entry_point_symbols)
108 goto_model.symbol_table.remove(entry_point_symbol);
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)
irep_idt mode
Language mode.
virtual void get_language_options(const cmdlinet &)
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
#define INVARIANT(CONDITION, REASON)
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)
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)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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