cprover
|
Interface providing access to a single function in a GOTO model, plus its associated symbol table. More...
#include <goto_model.h>
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_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 |
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.
|
inline |
Construct a function wrapper.
goto_model | will be used to ensure unique numbering of goto programs, specifically incrementing its unused_location_number member each time a program is re-numbered. |
goto_function | function to wrap. |
Definition at line 155 of file goto_model.h.
|
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.
|
inline |
Get function id.
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()().
|
inline |
Get GOTO function.
Definition at line 193 of file goto_model.h.
References goto_function.
Referenced by remove_returnst::operator()().
|
inline |
Get symbol table.
goto_function
. Definition at line 186 of file goto_model.h.
References symbol_table.
Referenced by remove_returns().
|
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.
|
private |
Definition at line 208 of file goto_model.h.
Referenced by get_function_id(), and update_instructions_function().
|
private |
Definition at line 209 of file goto_model.h.
Referenced by compute_location_numbers(), get_goto_function(), and update_instructions_function().
|
private |
Definition at line 207 of file goto_model.h.
Referenced by compute_location_numbers().
|
private |
Definition at line 206 of file goto_model.h.
Referenced by get_symbol_table().