cprover
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)
 
void unload (const irep_idt &name)
 
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) const
 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 24 of file goto_model.h.

Constructor & Destructor Documentation

◆ goto_modelt() [1/3]

goto_modelt::goto_modelt ( )
inline

Definition at line 40 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 54 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 87 of file goto_model.h.

◆ clear()

void goto_modelt::clear ( void  )
inline

Definition at line 34 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 81 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 71 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 76 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 60 of file goto_model.h.

◆ unload()

void goto_modelt::unload ( const irep_idt name)
inline

Definition at line 67 of file goto_model.h.

◆ validate()

void goto_modelt::validate ( const validation_modet  vm) const
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.

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


The documentation for this class was generated from the following file: