CBMC
goto_modelt Class Reference

#include <goto_model.h>

+ Inheritance diagram for goto_modelt:
+ Collaboration diagram for goto_modelt:

Public Member Functions

void clear ()
 
 goto_modelt ()
 
 goto_modelt (const goto_modelt &)=delete
 
goto_modeltoperator= (const goto_modelt &)=delete
 
 goto_modelt (goto_modelt &&other)
 
goto_modeltoperator= (goto_modelt &&other)
 
std::size_t unload (const irep_idt &name)
 Remove the function named name from the function map, if it exists. More...
 
const goto_functionstget_goto_functions () const override
 Accessor to get a raw goto_functionst. More...
 
const symbol_tabletget_symbol_table () const override
 Accessor to get the symbol table. More...
 
const goto_functionst::goto_functiontget_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=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
 Check that the goto model is well-formed. More...
 
- Public Member Functions inherited from abstract_goto_modelt
virtual ~abstract_goto_modelt ()
 

Public Attributes

symbol_tablet symbol_table
 Symbol table. More...
 
goto_functionst goto_functions
 GOTO functions. More...
 

Detailed Description

Definition at line 26 of file goto_model.h.

Constructor & Destructor Documentation

◆ goto_modelt() [1/3]

goto_modelt::goto_modelt ( )
inline

Definition at line 42 of file goto_model.h.

◆ goto_modelt() [2/3]

goto_modelt::goto_modelt ( const goto_modelt )
delete

◆ goto_modelt() [3/3]

goto_modelt::goto_modelt ( goto_modelt &&  other)
inline

Definition at line 56 of file goto_model.h.

Member Function Documentation

◆ can_produce_function()

bool goto_modelt::can_produce_function ( const irep_idt id) const
inlineoverridevirtual

Determines if this model can produce a body for the given function.

Parameters
idfunction 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 95 of file goto_model.h.

◆ clear()

void goto_modelt::clear ( void  )
inline

Definition at line 36 of file goto_model.h.

◆ get_goto_function()

const goto_functionst::goto_functiont& goto_modelt::get_goto_function ( const irep_idt id)
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
idfunction 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: