cprover
abstract_goto_modelt Class Referenceabstract

Abstract interface to eager or lazy GOTO models. More...

#include <abstract_goto_model.h>

Inheritance diagram for abstract_goto_modelt:
[legend]

Public Member Functions

virtual ~abstract_goto_modelt ()
 
virtual bool can_produce_function (const irep_idt &id) const =0
 Determines if this model can produce a body for the given function. More...
 
virtual const goto_functionst::goto_functiontget_goto_function (const irep_idt &id)=0
 Get a GOTO function by name, or throw if no such function exists. More...
 
virtual const goto_functionstget_goto_functions () const =0
 Accessor to get a raw goto_functionst. More...
 
virtual const symbol_tabletget_symbol_table () const =0
 Accessor to get the symbol table. More...
 

Detailed Description

Abstract interface to eager or lazy GOTO models.

Definition at line 19 of file abstract_goto_model.h.

Constructor & Destructor Documentation

◆ ~abstract_goto_modelt()

virtual abstract_goto_modelt::~abstract_goto_modelt ( )
inlinevirtual

Definition at line 22 of file abstract_goto_model.h.

Member Function Documentation

◆ can_produce_function()

virtual bool abstract_goto_modelt::can_produce_function ( const irep_idt id) const
pure virtual

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.

Implemented in wrapper_goto_modelt, lazy_goto_modelt, and goto_modelt.

Referenced by jbmc_parse_optionst::process_goto_function().

◆ get_goto_function()

virtual const goto_functionst::goto_functiont& abstract_goto_modelt::get_goto_function ( const irep_idt id)
pure virtual

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
function body

Implemented in lazy_goto_modelt, wrapper_goto_modelt, and goto_modelt.

Referenced by bmct::execute().

◆ get_goto_functions()

virtual const goto_functionst& abstract_goto_modelt::get_goto_functions ( ) const
pure virtual

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.

Implemented in lazy_goto_modelt, wrapper_goto_modelt, and goto_modelt.

Referenced by bmct::execute(), and jbmc_parse_optionst::show_loaded_functions().

◆ get_symbol_table()

virtual const symbol_tablet& abstract_goto_modelt::get_symbol_table ( ) const
pure virtual

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.

Implemented in lazy_goto_modelt, wrapper_goto_modelt, and goto_modelt.

Referenced by bmct::do_language_agnostic_bmc(), and jbmc_parse_optionst::show_loaded_functions().


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