cprover
goto_symex_statet Class Referencefinal

#include <goto_symex_state.h>

+ Collaboration diagram for goto_symex_statet:

Classes

struct  framet
 
class  goto_statet
 
struct  threadt
 

Public Types

enum  levelt { L0 =0, L1 =1, L2 =2 }
 
typedef std::list< goto_statetgoto_state_listt
 
typedef std::map< goto_programt::const_targett, goto_state_listtgoto_state_mapt
 
typedef std::vector< frametcall_stackt
 
typedef std::pair< unsigned, std::list< guardt > > a_s_r_entryt
 
typedef std::list< guardta_s_w_entryt
 

Public Member Functions

 goto_symex_statet ()
 
 ~goto_symex_statet ()
 
 goto_symex_statet (const goto_symex_statet &other, symex_target_equationt *const target)
 Fake "copy constructor" that initializes the symex_target member. More...
 
void output_propagation_map (std::ostream &)
 Print the constant propagation map in a human-friendly format. More...
 
void rename (exprt &expr, const namespacet &ns, levelt level=L2)
 
void rename (typet &type, const irep_idt &l1_identifier, const namespacet &ns, levelt level=L2)
 
void assignment (ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
 
void get_original_name (exprt &expr) const
 
void get_original_name (typet &type) const
 
 goto_symex_statet (const goto_statet &s)
 
call_stacktcall_stack ()
 
const call_stacktcall_stack () const
 
framettop ()
 
const framettop () const
 
frametnew_frame ()
 
void pop_frame ()
 
const frametprevious_frame ()
 
void print_backtrace (std::ostream &) const
 Dumps the current state of symex, printing the function name and location number for each stack frame in the currently active thread. More...
 
bool l2_thread_read_encoding (ssa_exprt &expr, const namespacet &ns)
 thread encoding More...
 
bool l2_thread_write_encoding (const ssa_exprt &expr, const namespacet &ns)
 thread encoding More...
 

Public Attributes

symbol_tablet symbol_table
 contains symbols that are minted during symbolic execution, such as dynamically created objects etc. More...
 
unsigned depth
 distance from entry More...
 
guardt guard
 
symex_targett::sourcet source
 
symex_target_equationtsymex_target
 
std::set< irep_idtl1_history
 
symex_level0t level0
 
symex_level1t level1
 
symex_level2t level2
 
std::map< irep_idt, exprtpropagation
 
std::unordered_map< irep_idt, local_safe_pointerstsafe_pointers
 
value_sett value_set
 
unsigned atomic_section_id
 
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hashread_in_atomic_section
 
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hashwritten_in_atomic_section
 
unsigned total_vccs
 
unsigned remaining_vccs
 
std::vector< threadtthreads
 
bool record_events
 
incremental_dirtyt dirty
 
goto_programt::const_targett saved_target
 
bool has_saved_jump_target
 This state is saved, with the PC pointing to the target of a GOTO. More...
 
bool has_saved_next_instruction
 This state is saved, with the PC pointing to the next instruction of a GOTO. More...
 
bool run_validation_checks
 Should the additional validation checks be run? More...
 

Protected Types

typedef std::unordered_map< irep_idt, typetl1_typest
 

Protected Member Functions

void rename_address (exprt &expr, const namespacet &ns, levelt level)
 
void set_l0_indices (ssa_exprt &expr, const namespacet &ns)
 
void set_l1_indices (ssa_exprt &expr, const namespacet &ns)
 
void set_l2_indices (ssa_exprt &expr, const namespacet &ns)
 

Protected Attributes

l1_typest l1_types
 

Private Member Functions

 goto_symex_statet (const goto_symex_statet &other)=default
 Dangerous, do not use. More...
 

Detailed Description

Definition at line 34 of file goto_symex_state.h.

Member Typedef Documentation

◆ a_s_r_entryt

typedef std::pair<unsigned, std::list<guardt> > goto_symex_statet::a_s_r_entryt

Definition at line 235 of file goto_symex_state.h.

◆ a_s_w_entryt

Definition at line 236 of file goto_symex_state.h.

◆ call_stackt

typedef std::vector<framet> goto_symex_statet::call_stackt

Definition at line 201 of file goto_symex_state.h.

◆ goto_state_listt

Definition at line 168 of file goto_symex_state.h.

◆ goto_state_mapt

◆ l1_typest

typedef std::unordered_map<irep_idt, typet> goto_symex_statet::l1_typest
protected

Definition at line 101 of file goto_symex_state.h.

Member Enumeration Documentation

◆ levelt

Enumerator
L0 
L1 
L2 

Definition at line 72 of file goto_symex_state.h.

Constructor & Destructor Documentation

◆ goto_symex_statet() [1/4]

goto_symex_statet::goto_symex_statet ( )

Definition at line 30 of file goto_symex_state.cpp.

◆ ~goto_symex_statet()

goto_symex_statet::~goto_symex_statet ( )
default

◆ goto_symex_statet() [2/4]

goto_symex_statet::goto_symex_statet ( const goto_symex_statet other,
symex_target_equationt *const  target 
)
inlineexplicit

Fake "copy constructor" that initializes the symex_target member.

Definition at line 41 of file goto_symex_state.h.

◆ goto_symex_statet() [3/4]

goto_symex_statet::goto_symex_statet ( const goto_statet s)
inlineexplicit

Definition at line 153 of file goto_symex_state.h.

◆ goto_symex_statet() [4/4]

goto_symex_statet::goto_symex_statet ( const goto_symex_statet other)
privatedefault

Dangerous, do not use.

Copying a state S1 to S2 risks S2 pointing to a deallocated symex_target_equationt if S1 (and the symex_target_equationt that its symex_target member points to) go out of scope. If your class has a goto_symex_statet member and needs a copy constructor, copy instances of this class using the public two-argument copy constructor constructor to ensure that the copy points to an allocated symex_target_equationt. The two-argument copy constructor uses this private copy constructor as a delegate.

Member Function Documentation

◆ assignment()

void goto_symex_statet::assignment ( ssa_exprt lhs,
const exprt rhs,
const namespacet ns,
bool  rhs_is_simplified,
bool  record_value,
bool  allow_pointer_unsoundness = false 
)

Definition at line 161 of file goto_symex_state.cpp.

◆ call_stack() [1/2]

call_stackt& goto_symex_statet::call_stack ( )
inline

Definition at line 203 of file goto_symex_state.h.

◆ call_stack() [2/2]

const call_stackt& goto_symex_statet::call_stack ( ) const
inline

Definition at line 209 of file goto_symex_state.h.

◆ get_original_name() [1/2]

void goto_symex_statet::get_original_name ( exprt expr) const

Definition at line 706 of file goto_symex_state.cpp.

◆ get_original_name() [2/2]

void goto_symex_statet::get_original_name ( typet type) const

Definition at line 718 of file goto_symex_state.cpp.

◆ l2_thread_read_encoding()

bool goto_symex_statet::l2_thread_read_encoding ( ssa_exprt expr,
const namespacet ns 
)

thread encoding

Definition at line 369 of file goto_symex_state.cpp.

◆ l2_thread_write_encoding()

bool goto_symex_statet::l2_thread_write_encoding ( const ssa_exprt expr,
const namespacet ns 
)

thread encoding

Definition at line 511 of file goto_symex_state.cpp.

◆ new_frame()

framet& goto_symex_statet::new_frame ( )
inline

Definition at line 227 of file goto_symex_state.h.

◆ output_propagation_map()

void goto_symex_statet::output_propagation_map ( std::ostream &  out)

Print the constant propagation map in a human-friendly format.

This is primarily for use from the debugger; please don't delete me just because there aren't any current callers.

Definition at line 786 of file goto_symex_state.cpp.

◆ pop_frame()

void goto_symex_statet::pop_frame ( )
inline

Definition at line 228 of file goto_symex_state.h.

◆ previous_frame()

const framet& goto_symex_statet::previous_frame ( )
inline

Definition at line 229 of file goto_symex_state.h.

◆ print_backtrace()

void goto_symex_statet::print_backtrace ( std::ostream &  out) const

Dumps the current state of symex, printing the function name and location number for each stack frame in the currently active thread.

This is for use from the debugger or in debug code; please don't delete it just because it isn't called at present.

Parameters
outstream to write to

Definition at line 759 of file goto_symex_state.cpp.

◆ rename() [1/2]

void goto_symex_statet::rename ( exprt expr,
const namespacet ns,
levelt  level = L2 
)

Definition at line 270 of file goto_symex_state.cpp.

◆ rename() [2/2]

void goto_symex_statet::rename ( typet type,
const irep_idt l1_identifier,
const namespacet ns,
levelt  level = L2 
)

Definition at line 626 of file goto_symex_state.cpp.

◆ rename_address()

void goto_symex_statet::rename_address ( exprt expr,
const namespacet ns,
levelt  level 
)
protected

Definition at line 546 of file goto_symex_state.cpp.

◆ set_l0_indices()

void goto_symex_statet::set_l0_indices ( ssa_exprt expr,
const namespacet ns 
)
protected

Definition at line 240 of file goto_symex_state.cpp.

◆ set_l1_indices()

void goto_symex_statet::set_l1_indices ( ssa_exprt expr,
const namespacet ns 
)
protected

Definition at line 247 of file goto_symex_state.cpp.

◆ set_l2_indices()

void goto_symex_statet::set_l2_indices ( ssa_exprt expr,
const namespacet ns 
)
protected

Definition at line 259 of file goto_symex_state.cpp.

◆ top() [1/2]

framet& goto_symex_statet::top ( )
inline

Definition at line 215 of file goto_symex_state.h.

◆ top() [2/2]

const framet& goto_symex_statet::top ( ) const
inline

Definition at line 221 of file goto_symex_state.h.

Member Data Documentation

◆ atomic_section_id

unsigned goto_symex_statet::atomic_section_id

Definition at line 234 of file goto_symex_state.h.

◆ depth

unsigned goto_symex_statet::depth

distance from entry

Definition at line 55 of file goto_symex_state.h.

◆ dirty

incremental_dirtyt goto_symex_statet::dirty

Definition at line 258 of file goto_symex_state.h.

◆ guard

guardt goto_symex_statet::guard

Definition at line 57 of file goto_symex_state.h.

◆ has_saved_jump_target

bool goto_symex_statet::has_saved_jump_target

This state is saved, with the PC pointing to the target of a GOTO.

Definition at line 263 of file goto_symex_state.h.

◆ has_saved_next_instruction

bool goto_symex_statet::has_saved_next_instruction

This state is saved, with the PC pointing to the next instruction of a GOTO.

Definition at line 267 of file goto_symex_state.h.

◆ l1_history

std::set<irep_idt> goto_symex_statet::l1_history

Definition at line 62 of file goto_symex_state.h.

◆ l1_types

l1_typest goto_symex_statet::l1_types
protected

Definition at line 102 of file goto_symex_state.h.

◆ level0

symex_level0t goto_symex_statet::level0

Definition at line 64 of file goto_symex_state.h.

◆ level1

symex_level1t goto_symex_statet::level1

Definition at line 65 of file goto_symex_state.h.

◆ level2

symex_level2t goto_symex_statet::level2

Definition at line 66 of file goto_symex_state.h.

◆ propagation

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

Definition at line 69 of file goto_symex_state.h.

◆ read_in_atomic_section

std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash> goto_symex_statet::read_in_atomic_section

Definition at line 237 of file goto_symex_state.h.

◆ record_events

bool goto_symex_statet::record_events

Definition at line 257 of file goto_symex_state.h.

◆ remaining_vccs

unsigned goto_symex_statet::remaining_vccs

Definition at line 241 of file goto_symex_state.h.

◆ run_validation_checks

bool goto_symex_statet::run_validation_checks

Should the additional validation checks be run?

Definition at line 270 of file goto_symex_state.h.

◆ safe_pointers

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

Definition at line 105 of file goto_symex_state.h.

◆ saved_target

goto_programt::const_targett goto_symex_statet::saved_target

Definition at line 260 of file goto_symex_state.h.

◆ source

symex_targett::sourcet goto_symex_statet::source

Definition at line 58 of file goto_symex_state.h.

◆ symbol_table

symbol_tablet goto_symex_statet::symbol_table

contains symbols that are minted during symbolic execution, such as dynamically created objects etc.

The names in this table are needed for error traces even after symbolic execution has finished.

Definition at line 52 of file goto_symex_state.h.

◆ symex_target

symex_target_equationt* goto_symex_statet::symex_target

Definition at line 59 of file goto_symex_state.h.

◆ threads

std::vector<threadt> goto_symex_statet::threads

Definition at line 252 of file goto_symex_state.h.

◆ total_vccs

unsigned goto_symex_statet::total_vccs

Definition at line 241 of file goto_symex_state.h.

◆ value_set

value_sett goto_symex_statet::value_set

Definition at line 109 of file goto_symex_state.h.

◆ written_in_atomic_section

std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash> goto_symex_statet::written_in_atomic_section

Definition at line 239 of file goto_symex_state.h.


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