cprover
|
#include <goto_symex_state.h>
Classes | |
struct | loop_infot |
Public Types | |
typedef std::set< irep_idt > | local_objectst |
typedef std::map< irep_idt, goto_programt::targett > | catch_mapt |
typedef std::unordered_map< irep_idt, loop_infot, irep_id_hash > | loop_iterationst |
Public Member Functions | |
framet () | |
Definition at line 236 of file goto_symex_state.h.
typedef std::map<irep_idt, goto_programt::targett> goto_symex_statet::framet::catch_mapt |
Definition at line 260 of file goto_symex_state.h.
typedef std::set<irep_idt> goto_symex_statet::framet::local_objectst |
Definition at line 250 of file goto_symex_state.h.
typedef std::unordered_map<irep_idt, loop_infot, irep_id_hash> goto_symex_statet::framet::loop_iterationst |
Definition at line 276 of file goto_symex_state.h.
|
inline |
Definition at line 253 of file goto_symex_state.h.
symex_targett::sourcet goto_symex_statet::framet::calling_location |
Definition at line 242 of file goto_symex_state.h.
Referenced by goto_symex_statet::initialize(), goto_symext::operator()(), and goto_symext::pop_frame().
catch_mapt goto_symex_statet::framet::catch_map |
Definition at line 261 of file goto_symex_state.h.
Referenced by goto_symext::symex_catch(), and goto_symext::symex_throw().
goto_programt::const_targett goto_symex_statet::framet::end_of_function |
Definition at line 244 of file goto_symex_state.h.
Referenced by goto_symex_statet::initialize(), and goto_symext::operator()().
irep_idt goto_symex_statet::framet::function_identifier |
Definition at line 240 of file goto_symex_state.h.
goto_state_mapt goto_symex_statet::framet::goto_state_map |
Definition at line 241 of file goto_symex_state.h.
Referenced by goto_symext::merge_gotos(), and goto_symext::symex_goto().
bool goto_symex_statet::framet::hidden_function |
Definition at line 246 of file goto_symex_state.h.
Referenced by goto_symext::symex_assign(), and goto_symext::symex_decl().
local_objectst goto_symex_statet::framet::local_objects |
Definition at line 251 of file goto_symex_state.h.
Referenced by goto_symext::locality(), goto_symext::pop_frame(), and goto_symext::symex_start_thread().
loop_iterationst goto_symex_statet::framet::loop_iterations |
Definition at line 277 of file goto_symex_state.h.
Referenced by goto_symext::symex_function_call_code(), goto_symext::symex_goto(), and goto_symext::symex_transition().
renaming_levelt::current_namest goto_symex_statet::framet::old_level1 |
Definition at line 248 of file goto_symex_state.h.
Referenced by goto_symext::locality(), and goto_symext::pop_frame().
exprt goto_symex_statet::framet::return_value |
Definition at line 245 of file goto_symex_state.h.
Referenced by goto_symext::return_assignment().