cprover
symex_slice_by_tracet Class Reference

#include <slice_by_trace.h>

Collaboration diagram for symex_slice_by_tracet:
[legend]

Public Member Functions

 symex_slice_by_tracet (const namespacet &_ns)
 
void slice_by_trace (std::string trace_files, symex_target_equationt &equation)
 

Protected Types

typedef std::set< irep_idtalphabett
 
typedef std::pair< std::set< irep_idt >, bool > event_sett
 
typedef std::vector< event_settevent_tracet
 
typedef std::vector< std::vector< irep_idt > > value_tracet
 
typedef std::vector< exprttrace_conditionst
 

Protected Member Functions

void read_trace (std::string filename)
 
bool parse_alphabet (std::string read_line)
 
void parse_events (std::string read_line)
 
void compute_ts_fd (symex_target_equationt &equation)
 
void compute_ts_back (symex_target_equationt &equation)
 
void slice_SSA_steps (symex_target_equationt &equation, std::set< exprt > implications)
 
bool matches (event_sett s, irep_idt event)
 
void assign_merges (symex_target_equationt &equation)
 
std::set< exprtimplied_guards (exprt e)
 
bool implies_false (exprt e)
 

Protected Attributes

const namespacetns
 
alphabett alphabet
 
bool alphabet_parity
 
std::string semantics
 
event_tracet sigma
 
value_tracet sigma_vals
 
trace_conditionst t
 
std::set< exprtsliced_guards
 
std::vector< exprtmerge_map_back
 
std::vector< std::pair< bool, std::set< exprt > > > merge_impl_cache_back
 
irep_idt merge_identifier
 
symbol_exprt merge_symbol
 

Detailed Description

Definition at line 17 of file slice_by_trace.h.

Member Typedef Documentation

◆ alphabett

typedef std::set<irep_idt> symex_slice_by_tracet::alphabett
protected

Definition at line 32 of file slice_by_trace.h.

◆ event_sett

typedef std::pair<std::set<irep_idt>, bool> symex_slice_by_tracet::event_sett
protected

Definition at line 37 of file slice_by_trace.h.

◆ event_tracet

typedef std::vector<event_sett> symex_slice_by_tracet::event_tracet
protected

Definition at line 38 of file slice_by_trace.h.

◆ trace_conditionst

typedef std::vector<exprt> symex_slice_by_tracet::trace_conditionst
protected

Definition at line 46 of file slice_by_trace.h.

◆ value_tracet

typedef std::vector<std::vector<irep_idt> > symex_slice_by_tracet::value_tracet
protected

Definition at line 42 of file slice_by_trace.h.

Constructor & Destructor Documentation

◆ symex_slice_by_tracet()

symex_slice_by_tracet::symex_slice_by_tracet ( const namespacet _ns)
inlineexplicit

Definition at line 20 of file slice_by_trace.h.

Member Function Documentation

◆ assign_merges()

◆ compute_ts_back()

◆ compute_ts_fd()

void symex_slice_by_tracet::compute_ts_fd ( symex_target_equationt equation)
protected

Definition at line 375 of file slice_by_trace.cpp.

◆ implied_guards()

std::set< exprt > symex_slice_by_tracet::implied_guards ( exprt  e)
protected

◆ implies_false()

bool symex_slice_by_tracet::implies_false ( exprt  e)
protected

Definition at line 620 of file slice_by_trace.cpp.

References implied_guards(), exprt::make_not(), ns, and simplify().

Referenced by compute_ts_back().

◆ matches()

bool symex_slice_by_tracet::matches ( event_sett  s,
irep_idt  event 
)
protected

Definition at line 497 of file slice_by_trace.cpp.

Referenced by compute_ts_back().

◆ parse_alphabet()

bool symex_slice_by_tracet::parse_alphabet ( std::string  read_line)
protected

Definition at line 165 of file slice_by_trace.cpp.

References alphabet, alphabet_parity, and semantics.

Referenced by read_trace().

◆ parse_events()

void symex_slice_by_tracet::parse_events ( std::string  read_line)
protected

Definition at line 185 of file slice_by_trace.cpp.

References alphabet, alphabet_parity, irept::find(), sigma, sigma_vals, and size_type().

Referenced by read_trace().

◆ read_trace()

void symex_slice_by_tracet::read_trace ( std::string  filename)
protected

◆ slice_by_trace()

◆ slice_SSA_steps()

void symex_slice_by_tracet::slice_SSA_steps ( symex_target_equationt equation,
std::set< exprt implications 
)
protected

Member Data Documentation

◆ alphabet

alphabett symex_slice_by_tracet::alphabet
protected

Definition at line 33 of file slice_by_trace.h.

Referenced by compute_ts_back(), parse_alphabet(), parse_events(), and read_trace().

◆ alphabet_parity

bool symex_slice_by_tracet::alphabet_parity
protected

Definition at line 34 of file slice_by_trace.h.

Referenced by compute_ts_back(), parse_alphabet(), parse_events(), and read_trace().

◆ merge_identifier

irep_idt symex_slice_by_tracet::merge_identifier
protected

Definition at line 56 of file slice_by_trace.h.

Referenced by slice_by_trace().

◆ merge_impl_cache_back

std::vector<std::pair<bool, std::set<exprt> > > symex_slice_by_tracet::merge_impl_cache_back
protected

Definition at line 54 of file slice_by_trace.h.

Referenced by compute_ts_back(), and implied_guards().

◆ merge_map_back

std::vector<exprt> symex_slice_by_tracet::merge_map_back
protected

Definition at line 52 of file slice_by_trace.h.

Referenced by assign_merges(), compute_ts_back(), and implied_guards().

◆ merge_symbol

symbol_exprt symex_slice_by_tracet::merge_symbol
protected

Definition at line 58 of file slice_by_trace.h.

Referenced by assign_merges(), compute_ts_back(), and slice_by_trace().

◆ ns

const namespacet& symex_slice_by_tracet::ns
protected

◆ semantics

std::string symex_slice_by_tracet::semantics
protected

Definition at line 35 of file slice_by_trace.h.

Referenced by compute_ts_back(), and parse_alphabet().

◆ sigma

event_tracet symex_slice_by_tracet::sigma
protected

Definition at line 40 of file slice_by_trace.h.

Referenced by compute_ts_back(), parse_events(), and read_trace().

◆ sigma_vals

value_tracet symex_slice_by_tracet::sigma_vals
protected

Definition at line 44 of file slice_by_trace.h.

Referenced by compute_ts_back(), parse_events(), and read_trace().

◆ sliced_guards

std::set<exprt> symex_slice_by_tracet::sliced_guards
protected

Definition at line 50 of file slice_by_trace.h.

Referenced by compute_ts_back(), and slice_by_trace().

◆ t

trace_conditionst symex_slice_by_tracet::t
protected

Definition at line 48 of file slice_by_trace.h.

Referenced by compute_ts_back(), read_trace(), and slice_by_trace().


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