cprover
|
Abstract interface to eager or lazy GOTO models. More...
#include <abstract_goto_model.h>
Public Member Functions | |
virtual | ~abstract_goto_modelt () |
virtual bool | can_produce_function (const irep_idt &id) const =0 |
Determines if this model can produce a body for the given function. More... | |
virtual const goto_functionst::goto_functiont & | get_goto_function (const irep_idt &id)=0 |
Get a GOTO function by name, or throw if no such function exists. More... | |
virtual const goto_functionst & | get_goto_functions () const =0 |
Accessor to get a raw goto_functionst. More... | |
virtual const symbol_tablet & | get_symbol_table () const =0 |
Accessor to get the symbol table. More... | |
Abstract interface to eager or lazy GOTO models.
Definition at line 19 of file abstract_goto_model.h.
|
inlinevirtual |
Definition at line 22 of file abstract_goto_model.h.
|
pure virtual |
Determines if this model can produce a body for the given function.
id | function ID to query |
Implemented in wrapper_goto_modelt, lazy_goto_modelt, and goto_modelt.
Referenced by jbmc_parse_optionst::process_goto_function().
|
pure virtual |
Get a GOTO function by name, or throw if no such function exists.
May have side-effects on the GOTO function map provided by get_goto_functions, or the symbol table returned by get_symbol_table, so iterators pointing into either may be invalidated.
id | function to get |
Implemented in lazy_goto_modelt, wrapper_goto_modelt, and goto_modelt.
Referenced by bmct::execute().
|
pure virtual |
Accessor to get a raw goto_functionst.
Concurrent use of get_goto_function may invalidate iterators or otherwise surprise users by modifying the map underneath them, so this should only be used to lend a reference to code that cannot also call get_goto_function.
Implemented in lazy_goto_modelt, wrapper_goto_modelt, and goto_modelt.
Referenced by bmct::execute(), and jbmc_parse_optionst::show_loaded_functions().
|
pure virtual |
Accessor to get the symbol table.
Concurrent use of get_goto_function may invalidate iterators or otherwise surprise users by modifying the map underneath them, so this should only be used to lend a reference to code that cannot also call get_goto_function.
Implemented in lazy_goto_modelt, wrapper_goto_modelt, and goto_modelt.
Referenced by bmct::do_language_agnostic_bmc(), and jbmc_parse_optionst::show_loaded_functions().