cprover
|
#include <goto_model.h>
Public Member Functions | |
void | clear () |
goto_modelt () | |
goto_modelt (const goto_modelt &)=delete | |
goto_modelt & | operator= (const goto_modelt &)=delete |
goto_modelt (goto_modelt &&other) | |
goto_modelt & | operator= (goto_modelt &&other) |
void | unload (const irep_idt &name) |
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 |
Check that the goto model is well-formed. More... | |
![]() | |
virtual | ~abstract_goto_modelt () |
Public Attributes | |
symbol_tablet | symbol_table |
Symbol table. More... | |
goto_functionst | goto_functions |
GOTO functions. More... | |
Definition at line 24 of file goto_model.h.
|
inline |
Definition at line 40 of file goto_model.h.
|
delete |
|
inline |
Definition at line 54 of file goto_model.h.
|
inlineoverridevirtual |
Determines if this model can produce a body for the given function.
id | function ID to query |
Implements abstract_goto_modelt.
Definition at line 87 of file goto_model.h.
|
inline |
Definition at line 34 of file goto_model.h.
|
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.
id | function to get |
Implements abstract_goto_modelt.
Definition at line 81 of file goto_model.h.
|
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 71 of file goto_model.h.
|
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 76 of file goto_model.h.
|
delete |
|
inline |
Definition at line 60 of file goto_model.h.
|
inline |
Definition at line 67 of file goto_model.h.
|
inline |
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.
Definition at line 97 of file goto_model.h.
goto_functionst goto_modelt::goto_functions |
GOTO functions.
Direct access is deprecated; use the abstract_goto_modelt interface instead if possible.
Definition at line 32 of file goto_model.h.
symbol_tablet goto_modelt::symbol_table |
Symbol table.
Direct access is deprecated; use the abstract_goto_modelt interface instead if possible.
Definition at line 29 of file goto_model.h.