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_modelt &	operator= (const goto_modelt &)=delete
	goto_modelt (goto_modelt &&other)
goto_modelt &	operator= (goto_modelt &&other)
std::size_t	unload (const irep_idt &name)
	Remove the function named name from the function map, if it exists.
const goto_functionst &	get_goto_functions () const override
	Accessor to get a raw goto_functionst.
const symbol_tablet &	get_symbol_table () const override
	Accessor to get the symbol table.
const goto_functionst::goto_functiont &	get_goto_function (const irep_idt &id) override
	Get a GOTO function by name, or throw if no such function exists.
bool	can_produce_function (const irep_idt &id) const override
	Determines if this model can produce a body for the given function.
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.
Public Member Functions inherited from abstract_goto_modelt
virtual	~abstract_goto_modelt ()

Public Attributes
symbol_tablet	symbol_table
	Symbol table.
goto_functionst	goto_functions
	GOTO functions.

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

id	function 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 ( )

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

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