CBMC
|
#include <interpreter_class.h>
Public Attributes | |
goto_programt::const_targett | return_pc |
goto_functionst::function_mapt::const_iterator | return_function |
mp_integer | return_value_address |
memory_mapt | local_map |
mp_integer | old_stack_pointer |
Definition at line 247 of file interpreter_class.h.
memory_mapt interpretert::stack_framet::local_map |
Definition at line 253 of file interpreter_class.h.
mp_integer interpretert::stack_framet::old_stack_pointer |
Definition at line 254 of file interpreter_class.h.
goto_functionst::function_mapt::const_iterator interpretert::stack_framet::return_function |
Definition at line 251 of file interpreter_class.h.
goto_programt::const_targett interpretert::stack_framet::return_pc |
Definition at line 250 of file interpreter_class.h.
mp_integer interpretert::stack_framet::return_value_address |
Definition at line 252 of file interpreter_class.h.