cprover
|
#include <slice_by_trace.h>
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_idt > | alphabett |
typedef std::pair< std::set< irep_idt >, bool > | event_sett |
typedef std::vector< event_sett > | event_tracet |
typedef std::vector< std::vector< irep_idt > > | value_tracet |
typedef std::vector< exprt > | trace_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_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< exprt > | implied_guards (exprt e) |
bool | implies_false (exprt e) |
Protected Attributes | |
const namespacet & | ns |
alphabett | alphabet |
bool | alphabet_parity |
std::string | semantics |
event_tracet | sigma |
value_tracet | sigma_vals |
trace_conditionst | t |
std::set< exprt > | sliced_guards |
std::vector< exprt > | merge_map_back |
std::vector< std::pair< bool, std::set< exprt > > > | merge_impl_cache_back |
irep_idt | merge_identifier |
symbol_exprt | merge_symbol |
Definition at line 17 of file slice_by_trace.h.
|
protected |
Definition at line 32 of file slice_by_trace.h.
|
protected |
Definition at line 37 of file slice_by_trace.h.
|
protected |
Definition at line 38 of file slice_by_trace.h.
|
protected |
Definition at line 46 of file slice_by_trace.h.
|
protected |
Definition at line 42 of file slice_by_trace.h.
|
inlineexplicit |
Definition at line 20 of file slice_by_trace.h.
|
protected |
Definition at line 496 of file slice_by_trace.cpp.
|
protected |
Definition at line 235 of file slice_by_trace.cpp.
Definition at line 525 of file slice_by_trace.cpp.
|
protected |
Definition at line 610 of file slice_by_trace.cpp.
|
protected |
Definition at line 488 of file slice_by_trace.cpp.
|
protected |
Definition at line 166 of file slice_by_trace.cpp.
|
protected |
Definition at line 186 of file slice_by_trace.cpp.
|
protected |
Definition at line 120 of file slice_by_trace.cpp.
void symex_slice_by_tracet::slice_by_trace | ( | std::string | trace_files, |
symex_target_equationt & | equation | ||
) |
Definition at line 28 of file slice_by_trace.cpp.
|
protected |
Definition at line 374 of file slice_by_trace.cpp.
|
protected |
Definition at line 33 of file slice_by_trace.h.
|
protected |
Definition at line 34 of file slice_by_trace.h.
|
protected |
Definition at line 56 of file slice_by_trace.h.
|
protected |
Definition at line 54 of file slice_by_trace.h.
|
protected |
Definition at line 52 of file slice_by_trace.h.
|
protected |
Definition at line 58 of file slice_by_trace.h.
|
protected |
Definition at line 31 of file slice_by_trace.h.
|
protected |
Definition at line 35 of file slice_by_trace.h.
|
protected |
Definition at line 40 of file slice_by_trace.h.
|
protected |
Definition at line 44 of file slice_by_trace.h.
|
protected |
Definition at line 50 of file slice_by_trace.h.
|
protected |
Definition at line 48 of file slice_by_trace.h.