cprover
|
#include <goto_symex_state.h>
Classes | |
struct | loop_infot |
Public Attributes | |
irep_idt | function_identifier |
goto_state_mapt | goto_state_map |
symex_targett::sourcet | calling_location |
goto_programt::const_targett | end_of_function |
exprt | return_value = nil_exprt() |
bool | hidden_function = false |
symex_renaming_levelt::current_namest | old_level1 |
std::set< irep_idt > | local_objects |
std::map< irep_idt, goto_programt::targett > | catch_map |
std::unordered_map< irep_idt, loop_infot > | loop_iterations |
Definition at line 174 of file goto_symex_state.h.
symex_targett::sourcet goto_symex_statet::framet::calling_location |
Definition at line 179 of file goto_symex_state.h.
std::map<irep_idt, goto_programt::targett> goto_symex_statet::framet::catch_map |
Definition at line 190 of file goto_symex_state.h.
goto_programt::const_targett goto_symex_statet::framet::end_of_function |
Definition at line 181 of file goto_symex_state.h.
irep_idt goto_symex_statet::framet::function_identifier |
Definition at line 177 of file goto_symex_state.h.
goto_state_mapt goto_symex_statet::framet::goto_state_map |
Definition at line 178 of file goto_symex_state.h.
bool goto_symex_statet::framet::hidden_function = false |
Definition at line 183 of file goto_symex_state.h.
std::set<irep_idt> goto_symex_statet::framet::local_objects |
Definition at line 187 of file goto_symex_state.h.
std::unordered_map<irep_idt, loop_infot> goto_symex_statet::framet::loop_iterations |
Definition at line 198 of file goto_symex_state.h.
symex_renaming_levelt::current_namest goto_symex_statet::framet::old_level1 |
Definition at line 185 of file goto_symex_state.h.
Definition at line 182 of file goto_symex_state.h.