cprover
goto_symex_statet::goto_statet Class Reference

#include <goto_symex_state.h>

+ Collaboration diagram for goto_symex_statet::goto_statet:

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
 
symex_level2t::current_namest level2_current_names
 
value_sett value_set
 
guardt guard
 
symex_targett::sourcet source
 
std::map< irep_idt, exprtpropagation
 
unsigned atomic_section_id
 
std::unordered_map< irep_idt, local_safe_pointerstsafe_pointers
 
unsigned total_vccs
 
unsigned remaining_vccs
 

Detailed Description

Definition at line 111 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 124 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 146 of file goto_symex_state.h.

◆ 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 139 of file goto_symex_state.h.

Member Data Documentation

◆ atomic_section_id

unsigned goto_symex_statet::goto_statet::atomic_section_id

Definition at line 120 of file goto_symex_state.h.

◆ depth

unsigned goto_symex_statet::goto_statet::depth

Definition at line 114 of file goto_symex_state.h.

◆ guard

guardt goto_symex_statet::goto_statet::guard

Definition at line 117 of file goto_symex_state.h.

◆ level2_current_names

symex_level2t::current_namest goto_symex_statet::goto_statet::level2_current_names

Definition at line 115 of file goto_symex_state.h.

◆ propagation

std::map<irep_idt, exprt> goto_symex_statet::goto_statet::propagation

Definition at line 119 of file goto_symex_state.h.

◆ remaining_vccs

unsigned goto_symex_statet::goto_statet::remaining_vccs

Definition at line 122 of file goto_symex_state.h.

◆ safe_pointers

std::unordered_map<irep_idt, local_safe_pointerst> goto_symex_statet::goto_statet::safe_pointers

Definition at line 121 of file goto_symex_state.h.

◆ source

symex_targett::sourcet goto_symex_statet::goto_statet::source

Definition at line 118 of file goto_symex_state.h.

◆ total_vccs

unsigned goto_symex_statet::goto_statet::total_vccs

Definition at line 122 of file goto_symex_state.h.

◆ value_set

value_sett goto_symex_statet::goto_statet::value_set

Definition at line 116 of file goto_symex_state.h.


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