cprover
goto_symex_statet::framet Struct Reference

#include <goto_symex_state.h>

+ Collaboration diagram for goto_symex_statet::framet:

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_idtlocal_objects
 
std::map< irep_idt, goto_programt::targettcatch_map
 
std::unordered_map< irep_idt, loop_infotloop_iterations
 

Detailed Description

Definition at line 174 of file goto_symex_state.h.

Member Data Documentation

◆ calling_location

symex_targett::sourcet goto_symex_statet::framet::calling_location

Definition at line 179 of file goto_symex_state.h.

◆ catch_map

std::map<irep_idt, goto_programt::targett> goto_symex_statet::framet::catch_map

Definition at line 190 of file goto_symex_state.h.

◆ end_of_function

goto_programt::const_targett goto_symex_statet::framet::end_of_function

Definition at line 181 of file goto_symex_state.h.

◆ function_identifier

irep_idt goto_symex_statet::framet::function_identifier

Definition at line 177 of file goto_symex_state.h.

◆ goto_state_map

goto_state_mapt goto_symex_statet::framet::goto_state_map

Definition at line 178 of file goto_symex_state.h.

◆ hidden_function

bool goto_symex_statet::framet::hidden_function = false

Definition at line 183 of file goto_symex_state.h.

◆ local_objects

std::set<irep_idt> goto_symex_statet::framet::local_objects

Definition at line 187 of file goto_symex_state.h.

◆ loop_iterations

std::unordered_map<irep_idt, loop_infot> goto_symex_statet::framet::loop_iterations

Definition at line 198 of file goto_symex_state.h.

◆ old_level1

symex_renaming_levelt::current_namest goto_symex_statet::framet::old_level1

Definition at line 185 of file goto_symex_state.h.

◆ return_value

exprt goto_symex_statet::framet::return_value = nil_exprt()

Definition at line 182 of file goto_symex_state.h.


The documentation for this struct was generated from the following file: