cprover
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:
[legend]

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...
 
void update_instructions_function ()
 Updates the empty function member of each instruction by setting them to function_id More...
 
journalling_symbol_tablet & get_symbol_table ()
 Get symbol table. More...
 
goto_functionst::goto_functiontget_goto_function ()
 Get GOTO function. More...
 
const irep_idtget_function_id ()
 Get function id. More...
 

Private Attributes

journalling_symbol_tablet & symbol_table
 
goto_functionstgoto_functions
 
irep_idt function_id
 
goto_functionst::goto_functiontgoto_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 147 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
goto_modelwill be used to ensure unique numbering of goto programs, specifically incrementing its unused_location_number member each time a program is re-numbered.
goto_functionfunction to wrap.

Definition at line 155 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 170 of file goto_model.h.

References goto_functionst::compute_location_numbers(), goto_function, and goto_functions.

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

References function_id.

Referenced by remove_returnst::operator()().

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

References goto_function.

Referenced by remove_returnst::operator()().

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

References symbol_table.

Referenced by remove_returns().

◆ update_instructions_function()

void goto_model_functiont::update_instructions_function ( )
inline

Updates the empty function member of each instruction by setting them to function_id

Definition at line 177 of file goto_model.h.

References function_id, and goto_function.

Member Data Documentation

◆ function_id

irep_idt goto_model_functiont::function_id
private

Definition at line 208 of file goto_model.h.

Referenced by get_function_id(), and update_instructions_function().

◆ goto_function

goto_functionst::goto_functiont& goto_model_functiont::goto_function
private

◆ goto_functions

goto_functionst& goto_model_functiont::goto_functions
private

Definition at line 207 of file goto_model.h.

Referenced by compute_location_numbers().

◆ symbol_table

journalling_symbol_tablet& goto_model_functiont::symbol_table
private

Definition at line 206 of file goto_model.h.

Referenced by get_symbol_table().


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