cprover
goto_symex_statet Class Referencefinal

#include <goto_symex_state.h>

+ Collaboration diagram for goto_symex_statet:

Classes

class  framet
 
class  goto_statet
 
struct  level0t
 
struct  level1t
 
struct  level2t
 
class  propagationt
 
struct  renaming_levelt
 
class  threadt
 

Public Types

enum  levelt { L0 =0, L1 =1, L2 =2 }
 
typedef std::map< irep_idt, irep_idtoriginal_identifierst
 
typedef std::set< irep_idtl1_historyt
 
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::unordered_map< ssa_exprt, a_s_r_entryt, irep_hashread_in_atomic_sectiont
 
typedef std::list< guardta_s_w_entryt
 
typedef std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hashwritten_in_atomic_sectiont
 
typedef std::vector< threadtthreadst
 

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 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 ()
 
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...
 
void populate_dirty_for_function (const irep_idt &id, const goto_functiont &)
 
void switch_to_thread (unsigned t)
 

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
 
l1_historyt l1_history
 
goto_symex_statet::level0t level0
 
goto_symex_statet::level1t level1
 
goto_symex_statet::level2t level2
 
class goto_symex_statet::propagationt propagation
 
std::unordered_map< irep_idt, local_safe_pointerstsafe_pointers
 
value_sett value_set
 
unsigned atomic_section_id
 
read_in_atomic_sectiont read_in_atomic_section
 
written_in_atomic_sectiont written_in_atomic_section
 
unsigned total_vccs
 
unsigned remaining_vccs
 
threadst threads
 
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 saved_target_is_backwards
 

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_ssa_indices (ssa_exprt &expr, const namespacet &ns, levelt level=L2)
 
void get_l1_name (exprt &expr) const
 

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 33 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 345 of file goto_symex_state.h.

◆ a_s_w_entryt

Definition at line 348 of file goto_symex_state.h.

◆ call_stackt

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

Definition at line 313 of file goto_symex_state.h.

◆ goto_state_listt

Definition at line 264 of file goto_symex_state.h.

◆ goto_state_mapt

◆ l1_historyt

Definition at line 65 of file goto_symex_state.h.

◆ l1_typest

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

Definition at line 193 of file goto_symex_state.h.

◆ original_identifierst

Definition at line 62 of file goto_symex_state.h.

◆ read_in_atomic_sectiont

Definition at line 347 of file goto_symex_state.h.

◆ threadst

typedef std::vector<threadt> goto_symex_statet::threadst

Definition at line 371 of file goto_symex_state.h.

◆ written_in_atomic_sectiont

Definition at line 350 of file goto_symex_state.h.

Member Enumeration Documentation

◆ levelt

Enumerator
L0 
L1 
L2 

Definition at line 164 of file goto_symex_state.h.

Constructor & Destructor Documentation

◆ goto_symex_statet() [1/4]

goto_symex_statet::goto_symex_statet ( )

Definition at line 26 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 40 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 249 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 229 of file goto_symex_state.cpp.

◆ call_stack() [1/2]

call_stackt& goto_symex_statet::call_stack ( )
inline

Definition at line 315 of file goto_symex_state.h.

◆ call_stack() [2/2]

const call_stackt& goto_symex_statet::call_stack ( ) const
inline

Definition at line 321 of file goto_symex_state.h.

◆ get_l1_name()

void goto_symex_statet::get_l1_name ( exprt expr) const
protected

Definition at line 832 of file goto_symex_state.cpp.

◆ get_original_name() [1/2]

void goto_symex_statet::get_original_name ( exprt expr) const

Definition at line 791 of file goto_symex_state.cpp.

◆ get_original_name() [2/2]

void goto_symex_statet::get_original_name ( typet type) const

Definition at line 803 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 448 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 593 of file goto_symex_state.cpp.

◆ new_frame()

framet& goto_symex_statet::new_frame ( )
inline

Definition at line 339 of file goto_symex_state.h.

◆ pop_frame()

void goto_symex_statet::pop_frame ( )
inline

Definition at line 340 of file goto_symex_state.h.

◆ populate_dirty_for_function()

void goto_symex_statet::populate_dirty_for_function ( const irep_idt id,
const goto_functiont  
)

◆ previous_frame()

const framet& goto_symex_statet::previous_frame ( )
inline

Definition at line 341 of file goto_symex_state.h.

◆ rename() [1/2]

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

Definition at line 354 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 708 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 628 of file goto_symex_state.cpp.

◆ set_ssa_indices()

void goto_symex_statet::set_ssa_indices ( ssa_exprt expr,
const namespacet ns,
levelt  level = L2 
)
protected

Definition at line 321 of file goto_symex_state.cpp.

◆ switch_to_thread()

void goto_symex_statet::switch_to_thread ( unsigned  t)

Definition at line 844 of file goto_symex_state.cpp.

◆ top() [1/2]

framet& goto_symex_statet::top ( )
inline

Definition at line 327 of file goto_symex_state.h.

◆ top() [2/2]

const framet& goto_symex_statet::top ( ) const
inline

Definition at line 333 of file goto_symex_state.h.

Member Data Documentation

◆ atomic_section_id

unsigned goto_symex_statet::atomic_section_id

Definition at line 344 of file goto_symex_state.h.

◆ depth

unsigned goto_symex_statet::depth

distance from entry

Definition at line 54 of file goto_symex_state.h.

◆ dirty

incremental_dirtyt goto_symex_statet::dirty

Definition at line 382 of file goto_symex_state.h.

◆ guard

guardt goto_symex_statet::guard

Definition at line 56 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 387 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 391 of file goto_symex_state.h.

◆ l1_history

l1_historyt goto_symex_statet::l1_history

Definition at line 66 of file goto_symex_state.h.

◆ l1_types

l1_typest goto_symex_statet::l1_types
protected

Definition at line 194 of file goto_symex_state.h.

◆ level0

goto_symex_statet::level0t goto_symex_statet::level0

◆ level1

goto_symex_statet::level1t goto_symex_statet::level1

◆ level2

goto_symex_statet::level2t goto_symex_statet::level2

◆ propagation

class goto_symex_statet::propagationt goto_symex_statet::propagation

◆ read_in_atomic_section

read_in_atomic_sectiont goto_symex_statet::read_in_atomic_section

Definition at line 351 of file goto_symex_state.h.

◆ record_events

bool goto_symex_statet::record_events

Definition at line 381 of file goto_symex_state.h.

◆ remaining_vccs

unsigned goto_symex_statet::remaining_vccs

Definition at line 354 of file goto_symex_state.h.

◆ safe_pointers

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

Definition at line 197 of file goto_symex_state.h.

◆ saved_target

goto_programt::const_targett goto_symex_statet::saved_target

Definition at line 384 of file goto_symex_state.h.

◆ saved_target_is_backwards

bool goto_symex_statet::saved_target_is_backwards

Definition at line 392 of file goto_symex_state.h.

◆ source

symex_targett::sourcet goto_symex_statet::source

Definition at line 57 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 51 of file goto_symex_state.h.

◆ symex_target

symex_target_equationt* goto_symex_statet::symex_target

Definition at line 58 of file goto_symex_state.h.

◆ threads

threadst goto_symex_statet::threads

Definition at line 372 of file goto_symex_state.h.

◆ total_vccs

unsigned goto_symex_statet::total_vccs

Definition at line 354 of file goto_symex_state.h.

◆ value_set

value_sett goto_symex_statet::value_set

Definition at line 201 of file goto_symex_state.h.

◆ written_in_atomic_section

written_in_atomic_sectiont goto_symex_statet::written_in_atomic_section

Definition at line 352 of file goto_symex_state.h.


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