12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H 13 #define CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H 222 #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
Wipe internal state of the symbol table.
goto_functionst::goto_functiont & goto_function
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto functions are well-formed.
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.
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
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.
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void validate(const validation_modet vm=validation_modet::INVARIANT) const
Check that the symbol table is well-formed.
::goto_functiont goto_functiont
const goto_functionst & goto_functions
A collection of goto functions.
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
void validate(const validation_modet vm) const
Check that the goto model is well-formed.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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)
Remove function from the function map.
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)
Interface providing access to a single function in a GOTO model, plus its associated symbol table.