#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)

void	unload (const irep_idt &name)

const goto_functionst &	get_goto_functions () const override
	Accessor to get a raw goto_functionst. More...

const symbol_tablet &	get_symbol_table () const override
	Accessor to get the symbol table. More...

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

Constructor & Destructor Documentation

◆ goto_modelt() [1/3]

goto_modelt::goto_modelt ( )

inline

Definition at line 41 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 55 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 88 of file goto_model.h.

◆ clear()

void goto_modelt::clear ( )

inline

Definition at line 35 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 82 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 72 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 77 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 61 of file goto_model.h.

◆ unload()

void goto_modelt::unload ( const irep_idt & name )

inline

Definition at line 68 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 98 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 33 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 30 of file goto_model.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/goto_model.h

Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ goto_modelt() [1/3]

◆ goto_modelt() [2/3]

◆ goto_modelt() [3/3]

Member Function Documentation

◆ can_produce_function()

◆ clear()

◆ get_goto_function()

◆ get_goto_functions()

◆ get_symbol_table()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ unload()

◆ validate()

Member Data Documentation

◆ goto_functions

◆ symbol_table