cprover
goto_symex_statet::framet Class Reference

#include <goto_symex_state.h>

Collaboration diagram for goto_symex_statet::framet:
[legend]

Classes

struct  loop_infot
 

Public Types

typedef std::set< irep_idtlocal_objectst
 
typedef std::map< irep_idt, goto_programt::targettcatch_mapt
 
typedef std::unordered_map< irep_idt, loop_infot, irep_id_hashloop_iterationst
 

Public Member Functions

 framet ()
 

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
 
bool hidden_function
 
renaming_levelt::current_namest old_level1
 
local_objectst local_objects
 
catch_mapt catch_map
 
loop_iterationst loop_iterations
 

Detailed Description

Definition at line 236 of file goto_symex_state.h.

Member Typedef Documentation

§ catch_mapt

§ local_objectst

Definition at line 250 of file goto_symex_state.h.

§ loop_iterationst

Definition at line 276 of file goto_symex_state.h.

Constructor & Destructor Documentation

§ framet()

goto_symex_statet::framet::framet ( )
inline

Definition at line 253 of file goto_symex_state.h.

Member Data Documentation

§ calling_location

symex_targett::sourcet goto_symex_statet::framet::calling_location

§ catch_map

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().

§ end_of_function

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()().

§ function_identifier

irep_idt goto_symex_statet::framet::function_identifier

Definition at line 240 of file goto_symex_state.h.

§ goto_state_map

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().

§ hidden_function

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_objects

local_objectst goto_symex_statet::framet::local_objects

§ loop_iterations

loop_iterationst goto_symex_statet::framet::loop_iterations

§ old_level1

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().

§ return_value

exprt goto_symex_statet::framet::return_value

Definition at line 245 of file goto_symex_state.h.

Referenced by goto_symext::return_assignment().


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