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_infotloop_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 263 of file goto_symex_state.h.

Member Typedef Documentation

◆ catch_mapt

◆ local_objectst

Definition at line 277 of file goto_symex_state.h.

◆ loop_iterationst

Definition at line 302 of file goto_symex_state.h.

Constructor & Destructor Documentation

◆ framet()

goto_symex_statet::framet::framet ( )
inline

Definition at line 280 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 288 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

◆ function_identifier

irep_idt goto_symex_statet::framet::function_identifier

Definition at line 267 of file goto_symex_state.h.

◆ goto_state_map

goto_state_mapt goto_symex_statet::framet::goto_state_map

Definition at line 268 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 273 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 275 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 272 of file goto_symex_state.h.

Referenced by goto_symext::return_assignment().


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