goto_model_functiont Class Reference

Interface providing access to a single function in a GOTO model, plus its associated symbol table. More...

#include <goto_model.h>

Collaboration diagram for goto_model_functiont:

Public Member Functions
	goto_model_functiont (journalling_symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function)
	Construct a function wrapper. More...
void	compute_location_numbers ()
	Re-number our goto_function. More...
journalling_symbol_tablet &	get_symbol_table ()
	Get symbol table. More...
goto_functionst::goto_functiont &	get_goto_function ()
	Get GOTO function. More...
const irep_idt &	get_function_id ()
	Get function id. More...

Private Attributes
journalling_symbol_tablet &	symbol_table
goto_functionst &	goto_functions
irep_idt	function_id
goto_functionst::goto_functiont &	goto_function

Detailed Description

Interface providing access to a single function in a GOTO model, plus its associated symbol table.

Its purpose is to permit GOTO program renumbering (a non-const operation on goto_functionst) without providing a non-const reference to the entire function map. For example, incremental function loading uses this, as in that situation functions other than the one currently being loaded should not be altered.

Definition at line 189 of file goto_model.h.

Constructor & Destructor Documentation

goto_model_functiont()

goto_model_functiont::goto_model_functiont ( journalling_symbol_tablet &  symbol_table, goto_functionst &  goto_functions, const irep_idt &  function_id, goto_functionst::goto_functiont &  goto_function  )

inline

Construct a function wrapper.

Parameters

symbol_table	Symbol table where any new symbols associated with goto_function should be inserted
goto_functions	goto_functionst that contains goto_function. Only used to ensure unique numbering of goto_function, specifically incrementing its unused_location_number member each time the program is re-numbered.
function_id	Name of function to wrap
goto_function	Function to wrap

Definition at line 201 of file goto_model.h.

Member Function Documentation

compute_location_numbers()

void goto_model_functiont::compute_location_numbers ( )

inline

Re-number our goto_function.

After this method returns all instructions' location numbers may have changed, but will be globally unique and in program order within the program.

Definition at line 216 of file goto_model.h.

get_function_id()

const irep_idt& goto_model_functiont::get_function_id ( )

inline

Get function id.

Returns

goto_function's name (its key in goto_functions)

Definition at line 239 of file goto_model.h.

get_goto_function()

goto_functionst::goto_functiont& goto_model_functiont::get_goto_function ( )

inline

Get GOTO function.

Returns

the wrapped GOTO function

Definition at line 232 of file goto_model.h.

get_symbol_table()

journalling_symbol_tablet& goto_model_functiont::get_symbol_table ( )

inline

Get symbol table.

Returns

journalling symbol table that (a) wraps the global symbol table, and (b) has recorded all symbol mutations (insertions, updates and deletions) that resulted from creating goto_function.

Definition at line 225 of file goto_model.h.

Member Data Documentation

function_id

irep_idt goto_model_functiont::function_id

private

Definition at line 247 of file goto_model.h.

goto_function

goto_functionst::goto_functiont& goto_model_functiont::goto_function

private

Definition at line 248 of file goto_model.h.

goto_functions

goto_functionst& goto_model_functiont::goto_functions

private

Definition at line 246 of file goto_model.h.

symbol_table

journalling_symbol_tablet& goto_model_functiont::symbol_table

private

Definition at line 245 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