12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H 13 #define CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H 212 #endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H Abstract interface to eager or lazy GOTO models.
const irep_idt & get_function_id()
Get function id.
void update_instructions_function()
Updates the empty function member of each instruction by setting them to function_id ...
virtual void clear() override
goto_functionst::goto_functiont & goto_function
Goto Programs with Functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
journalling_symbol_tablet & symbol_table
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
goto_modelt & operator=(goto_modelt &&other)
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Abstract interface to eager or lazy GOTO models.
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
void compute_location_numbers()
wrapper_goto_modelt(const symbol_tablet &symbol_table, const goto_functionst &goto_functions)
const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function by name, or throw if no such function exists.
void output(const namespacet &ns, std::ostream &out) const
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
::goto_functiont goto_functiont
const goto_functionst & goto_functions
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
goto_modelt & operator=(const goto_modelt &)=delete
const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function by name, or throw if no such function exists.
const symbol_tablet & symbol_table
void unload(const irep_idt &name)
void unload(const irep_idt &name)
Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst...
goto_model_functiont(journalling_symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function)
Construct a function wrapper.
goto_functionst & goto_functions
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
goto_functionst goto_functions
GOTO functions.
void compute_location_numbers()
Re-number our goto_function.
goto_modelt(goto_modelt &&other)
void output(std::ostream &out) const
Interface providing access to a single function in a GOTO model, plus its associated symbol table...