cprover
path_symex_statet Struct Reference

#include <path_symex_state.h>

Collaboration diagram for path_symex_statet:
[legend]

Classes

struct  framet
 
struct  threadt
 
struct  var_statet
 

Public Types

typedef path_symex_stept stept
 
typedef std::vector< var_statetvar_valt
 
typedef std::map< unsigned, var_statetvar_state_mapt
 
typedef std::vector< frametcall_stackt
 
typedef std::vector< threadtthreadst
 
typedef std::map< loc_reft, unsigned > unwinding_mapt
 
typedef std::map< irep_idt, unsigned > recursion_mapt
 

Public Member Functions

 path_symex_statet (var_mapt &_var_map, const locst &_locs, path_symex_historyt &_path_symex_history)
 
var_statetget_var_state (const var_mapt::var_infot &var_info)
 
unsigned get_current_thread () const
 
void set_current_thread (unsigned _thread)
 
goto_programt::const_targett get_instruction () const
 
bool is_executable () const
 
void record_step ()
 
threadtadd_thread ()
 
void disable_current_thread ()
 
loc_reft pc () const
 
void next_pc ()
 
void set_pc (loc_reft new_pc)
 
void output (std::ostream &out) const
 
void output (const threadt &thread, std::ostream &out) const
 
exprt read (const exprt &src)
 
exprt read_no_propagate (const exprt &src)
 
exprt dereference_rec (const exprt &src, bool propagate)
 
std::string array_index_as_string (const exprt &) const
 
unsigned get_no_thread_interleavings () const
 
unsigned get_depth () const
 
unsigned get_no_branches () const
 
bool last_was_branch () const
 
bool is_feasible (class decision_proceduret &) const
 
bool check_assertion (class decision_proceduret &)
 

Public Attributes

var_maptvar_map
 
const locstlocs
 
var_valt shared_vars
 
threadst threads
 
bool inside_atomic_section
 
path_symex_step_reft history
 
unwinding_mapt unwinding_map
 
recursion_mapt recursion_map
 

Protected Member Functions

exprt read (const exprt &src, bool propagate)
 
exprt instantiate_rec (const exprt &src, bool propagate)
 
exprt expand_structs_and_arrays (const exprt &src)
 
exprt array_theory (const exprt &src, bool propagate)
 
exprt instantiate_rec_address (const exprt &src, bool propagate)
 
exprt read_symbol_member_index (const exprt &src, bool propagate)
 
bool is_symbol_member_index (const exprt &src) const
 

Protected Attributes

unsigned current_thread
 
unsigned no_thread_interleavings
 
unsigned no_branches
 
unsigned depth
 

Detailed Description

Definition at line 21 of file path_symex_state.h.

Member Typedef Documentation

§ call_stackt

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

Definition at line 82 of file path_symex_state.h.

§ recursion_mapt

typedef std::map<irep_idt, unsigned> path_symex_statet::recursion_mapt

Definition at line 211 of file path_symex_state.h.

§ stept

Definition at line 39 of file path_symex_state.h.

§ threadst

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

Definition at line 98 of file path_symex_state.h.

§ unwinding_mapt

typedef std::map<loc_reft, unsigned> path_symex_statet::unwinding_mapt

Definition at line 207 of file path_symex_state.h.

§ var_state_mapt

typedef std::map<unsigned, var_statet> path_symex_statet::var_state_mapt

Definition at line 69 of file path_symex_state.h.

§ var_valt

Definition at line 65 of file path_symex_state.h.

Constructor & Destructor Documentation

§ path_symex_statet()

path_symex_statet::path_symex_statet ( var_mapt _var_map,
const locst _locs,
path_symex_historyt _path_symex_history 
)
inline

Definition at line 24 of file path_symex_state.h.

Member Function Documentation

§ add_thread()

threadt& path_symex_statet::add_thread ( )
inline

Definition at line 135 of file path_symex_state.h.

Referenced by initial_state(), and path_symext::operator()().

§ array_index_as_string()

std::string path_symex_statet::array_index_as_string ( const exprt src) const

§ array_theory()

§ check_assertion()

§ dereference_rec()

exprt path_symex_statet::dereference_rec ( const exprt src,
bool  propagate 
)

§ disable_current_thread()

void path_symex_statet::disable_current_thread ( )
inline

Definition at line 141 of file path_symex_state.h.

References current_thread.

Referenced by path_symext::operator()(), and path_symext::return_from_function().

§ expand_structs_and_arrays()

§ get_current_thread()

§ get_depth()

unsigned path_symex_statet::get_depth ( ) const
inline

Definition at line 187 of file path_symex_state.h.

References depth.

Referenced by path_searcht::drop_state(), and path_searcht::operator()().

§ get_instruction()

§ get_no_branches()

unsigned path_symex_statet::get_no_branches ( ) const
inline

Definition at line 192 of file path_symex_state.h.

References no_branches.

Referenced by path_searcht::drop_state().

§ get_no_thread_interleavings()

unsigned path_symex_statet::get_no_thread_interleavings ( ) const
inline

Definition at line 182 of file path_symex_state.h.

References no_thread_interleavings.

Referenced by path_searcht::drop_state().

§ get_var_state()

§ instantiate_rec()

§ instantiate_rec_address()

§ is_executable()

bool path_symex_statet::is_executable ( ) const
inline

Definition at line 121 of file path_symex_state.h.

References current_thread.

Referenced by path_searcht::operator()().

§ is_feasible()

bool path_symex_statet::is_feasible ( class decision_proceduret decision_procedure) const

§ is_symbol_member_index()

bool path_symex_statet::is_symbol_member_index ( const exprt src) const
protected

§ last_was_branch()

bool path_symex_statet::last_was_branch ( ) const
inline

§ next_pc()

void path_symex_statet::next_pc ( )
inline

§ output() [1/2]

void path_symex_statet::output ( std::ostream &  out) const

Definition at line 56 of file path_symex_state.cpp.

References threads.

Referenced by set_pc().

§ output() [2/2]

void path_symex_statet::output ( const threadt thread,
std::ostream &  out 
) const

§ pc()

loc_reft path_symex_statet::pc ( ) const
inline

§ read() [1/2]

§ read() [2/2]

exprt path_symex_statet::read ( const exprt src,
bool  propagate 
)
protected

§ read_no_propagate()

exprt path_symex_statet::read_no_propagate ( const exprt src)
inline

Definition at line 173 of file path_symex_state.h.

References array_index_as_string(), dereference_rec(), and read().

Referenced by path_symext::assign().

§ read_symbol_member_index()

§ record_step()

§ set_current_thread()

void path_symex_statet::set_current_thread ( unsigned  _thread)
inline

Definition at line 111 of file path_symex_state.h.

References current_thread.

Referenced by initial_state().

§ set_pc()

void path_symex_statet::set_pc ( loc_reft  new_pc)
inline

Definition at line 157 of file path_symex_state.h.

References current_thread, and output().

Referenced by path_symext::do_goto().

Member Data Documentation

§ current_thread

unsigned path_symex_statet::current_thread
protected

§ depth

unsigned path_symex_statet::depth
protected

Definition at line 218 of file path_symex_state.h.

Referenced by get_depth(), and record_step().

§ history

§ inside_atomic_section

bool path_symex_statet::inside_atomic_section

Definition at line 104 of file path_symex_state.h.

Referenced by path_symext::operator()().

§ locs

const locst& path_symex_statet::locs

§ no_branches

unsigned path_symex_statet::no_branches
protected

Definition at line 217 of file path_symex_state.h.

Referenced by get_no_branches(), and record_step().

§ no_thread_interleavings

unsigned path_symex_statet::no_thread_interleavings
protected

Definition at line 216 of file path_symex_state.h.

Referenced by get_no_thread_interleavings(), and record_step().

§ recursion_map

recursion_mapt path_symex_statet::recursion_map

§ shared_vars

var_valt path_symex_statet::shared_vars

Definition at line 66 of file path_symex_state.h.

Referenced by get_var_state().

§ threads

§ unwinding_map

unwinding_mapt path_symex_statet::unwinding_map

Definition at line 208 of file path_symex_state.h.

Referenced by path_symext::do_goto(), and path_searcht::drop_state().

§ var_map


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