path_symex_statet::framet Struct Reference

#include <path_symex_state.h>

Collaboration diagram for path_symex_statet::framet:

Public Attributes
irep_idt	current_function
loc_reft	return_location
exprt	return_lhs
exprt	return_rhs
var_state_mapt	saved_local_vars

Detailed Description

Definition at line 72 of file path_symex_state.h.

Member Data Documentation

current_function

irep_idt path_symex_statet::framet::current_function

Definition at line 74 of file path_symex_state.h.

return_lhs

exprt path_symex_statet::framet::return_lhs

Definition at line 76 of file path_symex_state.h.

return_location

loc_reft path_symex_statet::framet::return_location

Definition at line 75 of file path_symex_state.h.

return_rhs

exprt path_symex_statet::framet::return_rhs

Definition at line 77 of file path_symex_state.h.

saved_local_vars

var_state_mapt path_symex_statet::framet::saved_local_vars

Definition at line 78 of file path_symex_state.h.

---

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

• path-symex/path_symex_state.h