Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst. More...
#include <goto_model.h>
Inheritance diagram for wrapper_goto_modelt: Collaboration diagram for wrapper_goto_modelt:Public Member Functions | |
| wrapper_goto_modelt (const symbol_tablet &symbol_table, const goto_functionst &goto_functions) | |
| const goto_functionst & | get_goto_functions () const override |
| Accessor to get a raw goto_functionst. More... | |
| const symbol_tablet & | get_symbol_table () const override |
| Accessor to get the symbol table. More... | |
| 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. More... | |
| bool | can_produce_function (const irep_idt &id) const override |
| Determines if this model can produce a body for the given function. More... | |
| void | validate (const validation_modet vm, const goto_model_validation_optionst &goto_model_validation_options) const override |
| Check that the goto model is well-formed. More... | |
| Public Member Functions inherited from abstract_goto_modelt | |
| virtual | ~abstract_goto_modelt () |
Private Attributes | |
| const symbol_tablet & | symbol_table |
| const goto_functionst & | goto_functions |
Detailed Description
Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst.
Definition at line 124 of file goto_model.h.
Constructor & Destructor Documentation
◆ wrapper_goto_modelt()
|
inline |
Definition at line 127 of file goto_model.h.
Member Function Documentation
◆ can_produce_function()
|
inlineoverridevirtual |
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.
Implements abstract_goto_modelt.
Definition at line 151 of file goto_model.h.
◆ get_goto_function()
|
inlineoverridevirtual |
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
Implements abstract_goto_modelt.
Definition at line 145 of file goto_model.h.
◆ get_goto_functions()
|
inlineoverridevirtual |
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.
Implements abstract_goto_modelt.
Definition at line 135 of file goto_model.h.
◆ get_symbol_table()
|
inlineoverridevirtual |
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.
Implements abstract_goto_modelt.
Definition at line 140 of file goto_model.h.
◆ validate()
|
inlineoverridevirtual |
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.
Implements abstract_goto_modelt.
Definition at line 161 of file goto_model.h.
Member Data Documentation
◆ goto_functions
|
private |
Definition at line 179 of file goto_model.h.
◆ symbol_table
|
private |
Definition at line 178 of file goto_model.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/goto-programs/goto_model.h
