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 153 of file goto_model.h.
|
inline |
Construct a function wrapper.
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 165 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 180 of file goto_model.h.
|
inline |
Get function id.
goto_function
's name (its key in goto_functions
) Definition at line 210 of file goto_model.h.
|
inline |
|
inline |
Get symbol table.
goto_function
. Definition at line 196 of file goto_model.h.
|
inline |
Updates the empty function member of each instruction by setting them to function_id
Definition at line 187 of file goto_model.h.
|
private |
Definition at line 218 of file goto_model.h.
|
private |
Definition at line 219 of file goto_model.h.
|
private |
Definition at line 217 of file goto_model.h.
|
private |
Definition at line 216 of file goto_model.h.