cprover
|
#include <goto_model.h>
Public Attributes | |
symbol_tablet | symbol_table |
Symbol table. | |
goto_functionst | goto_functions |
GOTO functions. | |
Definition at line 25 of file goto_model.h.
|
inline |
Definition at line 41 of file goto_model.h.
|
delete |
|
inline |
Definition at line 55 of file goto_model.h.
Determines if this model can produce a body for the given function.
id | function ID to query |
Implements abstract_goto_modelt.
Definition at line 88 of file goto_model.h.
|
inline |
Definition at line 35 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 82 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 72 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 77 of file goto_model.h.
|
delete |
|
inline |
Definition at line 61 of file goto_model.h.
Definition at line 68 of file goto_model.h.
|
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 98 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 33 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 30 of file goto_model.h.