Abstract interface to eager or lazy GOTO models. More...
#include <abstract_goto_model.h>
Inheritance diagram for abstract_goto_modelt: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... | |
| virtual void | validate (const validation_modet vm, const goto_model_validation_optionst &goto_model_validation_options) const =0 |
| Check that the goto model is well-formed. More... | |
Detailed Description
Abstract interface to eager or lazy GOTO models.
Definition at line 21 of file abstract_goto_model.h.
Constructor & Destructor Documentation
◆ ~abstract_goto_modelt()
|
inlinevirtual |
Definition at line 24 of file abstract_goto_model.h.
Member Function Documentation
◆ can_produce_function()
|
pure virtual |
Determines if this model can produce a body for the given function.
- Parameters
-
id function ID to query
- Returns
- true if we can produce a function body, or false if we would leave it a bodyless stub.
Implemented in wrapper_goto_modelt, goto_modelt, and lazy_goto_modelt.
◆ get_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.
- Parameters
-
id function to get
- Returns
- goto function
Implemented in wrapper_goto_modelt, goto_modelt, and lazy_goto_modelt.
◆ get_goto_functions()
|
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 wrapper_goto_modelt, goto_modelt, and lazy_goto_modelt.
◆ get_symbol_table()
|
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 wrapper_goto_modelt, goto_modelt, and lazy_goto_modelt.
◆ validate()
|
pure virtual |
Check that the goto model is well-formed.
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.
Implemented in goto_modelt, lazy_goto_modelt, and wrapper_goto_modelt.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/goto-programs/abstract_goto_model.h
