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 89 of file goto_model.h.

◆ get_goto_functions()

const goto_functionst & goto_modelt::get_goto_functions ( ) const

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 79 of file goto_model.h.

◆ get_symbol_table()

const symbol_tablet & goto_modelt::get_symbol_table ( ) const

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 84 of file goto_model.h.

◆ operator=() [1/2]

goto_modelt & goto_modelt::operator= ( const goto_modelt & )

delete

◆ operator=() [2/2]

goto_modelt & goto_modelt::operator= ( goto_modelt && other )

inline

Definition at line 62 of file goto_model.h.

◆ unload()

std::size_t goto_modelt::unload ( const irep_idt & name )

inline

Remove the function named name from the function map, if it exists.

Returns: Returns 0 when name was not present, and 1 when name was removed.

Definition at line 72 of file goto_model.h.

◆ validate()

void goto_modelt::validate ( const validation_modet vm = validation_modet::INVARIANT ,

const goto_model_validation_optionst & goto_model_validation_options = goto_model_validation_optionst{}

) const

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 105 of file goto_model.h.

Member Data Documentation

◆ goto_functions

goto_functionst goto_modelt::goto_functions

GOTO functions.

Direct access is deprecated; use the abstract_goto_modelt interface instead if possible.

Definition at line 34 of file goto_model.h.

◆ symbol_table

symbol_tablet goto_modelt::symbol_table

Symbol table.

Direct access is deprecated; use the abstract_goto_modelt interface instead if possible.

Definition at line 31 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