cprover
goto_symex_statet::goto_statet Class Reference

#include <goto_symex_state.h>

Collaboration diagram for goto_symex_statet::goto_statet:
[legend]

Public Member Functions

 goto_statet (const goto_symex_statet &s)
 
void level2_get_variables (std::unordered_set< ssa_exprt, irep_hash > &vars) const
 
unsigned level2_current_count (const irep_idt &identifier) const
 

Public Attributes

unsigned depth
 
level2t::current_namest level2_current_names
 
value_sett value_set
 
guardt guard
 
symex_targett::sourcet source
 
propagationt propagation
 
unsigned atomic_section_id
 

Detailed Description

Definition at line 204 of file goto_symex_state.h.

Constructor & Destructor Documentation

◆ goto_statet()

goto_symex_statet::goto_statet::goto_statet ( const goto_symex_statet s)
inlineexplicit

Definition at line 215 of file goto_symex_state.h.

Member Function Documentation

◆ level2_current_count()

unsigned goto_symex_statet::goto_statet::level2_current_count ( const irep_idt identifier) const
inline

Definition at line 237 of file goto_symex_state.h.

References level2_current_names.

Referenced by goto_symext::phi_function().

◆ level2_get_variables()

void goto_symex_statet::goto_statet::level2_get_variables ( std::unordered_set< ssa_exprt, irep_hash > &  vars) const
inline

Definition at line 227 of file goto_symex_state.h.

References level2_current_names.

Referenced by goto_symext::phi_function().

Member Data Documentation

◆ atomic_section_id

unsigned goto_symex_statet::goto_statet::atomic_section_id

Definition at line 213 of file goto_symex_state.h.

Referenced by goto_symext::merge_goto().

◆ depth

unsigned goto_symex_statet::goto_statet::depth

Definition at line 207 of file goto_symex_state.h.

Referenced by goto_symext::merge_goto().

◆ guard

guardt goto_symex_statet::goto_statet::guard

◆ level2_current_names

level2t::current_namest goto_symex_statet::goto_statet::level2_current_names

◆ propagation

propagationt goto_symex_statet::goto_statet::propagation

Definition at line 212 of file goto_symex_state.h.

Referenced by goto_symext::phi_function().

◆ source

symex_targett::sourcet goto_symex_statet::goto_statet::source

Definition at line 211 of file goto_symex_state.h.

Referenced by symex_bmct::merge_goto().

◆ value_set

value_sett goto_symex_statet::goto_statet::value_set

Definition at line 209 of file goto_symex_state.h.

Referenced by goto_symext::merge_value_sets().


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