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 500 of file slice_by_trace.cpp.
References guardt::as_expr(), goto_trace_stept::ASSIGNMENT, symex_target_equationt::SSA_stept::assignment_type, symex_target_equationt::SSA_stept::cond_expr, symex_target_equationt::SSA_stept::guard, symex_targett::HIDDEN, exprt::make_true(), merge_map_back, merge_symbol, ssa_exprt::set_level_2(), symex_target_equationt::SSA_stept::source, symex_target_equationt::SSA_stept::ssa_lhs, symex_target_equationt::SSA_stept::ssa_rhs, symex_target_equationt::SSA_steps, irept::swap(), and symex_target_equationt::SSA_stept::type.
Referenced by slice_by_trace().
|
protected |
Definition at line 233 of file slice_by_trace.cpp.
References alphabet, alphabet_parity, exprt::copy_to_operands(), format(), from_integer(), id2string(), implies_false(), exprt::is_false(), is_true(), exprt::make_not(), matches(), merge_impl_cache_back, merge_map_back, merge_symbol, exprt::move_to_operands(), ns, exprt::op0(), exprt::operands(), semantics, ssa_exprt::set_level_2(), sigma, sigma_vals, simplify(), sliced_guards, symex_target_equationt::SSA_steps, irept::swap(), t, and unsafe_string2int().
Referenced by slice_by_trace().
Definition at line 530 of file slice_by_trace.cpp.
References Forall_operands, irept::id(), id2string(), id_string, merge_impl_cache_back, merge_map_back, ns, r, simplify(), size_type(), to_symbol_expr(), and unsafe_string2size_t().
Referenced by implies_false(), and slice_by_trace().
|
protected |
Definition at line 615 of file slice_by_trace.cpp.
References implied_guards(), exprt::make_not(), ns, and simplify().
Referenced by compute_ts_back().
|
protected |
Definition at line 492 of file slice_by_trace.cpp.
Referenced by compute_ts_back().
|
protected |
Definition at line 165 of file slice_by_trace.cpp.
References alphabet, alphabet_parity, and semantics.
Referenced by read_trace().
|
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().
|
protected |
Definition at line 120 of file slice_by_trace.cpp.
References alphabet, alphabet_parity, get_nil_irep(), parse_alphabet(), parse_events(), sigma, sigma_vals, and t.
Referenced by slice_by_trace().
void symex_slice_by_tracet::slice_by_trace | ( | std::string | trace_files, |
symex_target_equationt & | equation | ||
) |
Definition at line 26 of file slice_by_trace.cpp.
References guardt::as_expr(), assign_merges(), goto_trace_stept::ASSUME, compute_ts_back(), symex_target_equationt::SSA_stept::cond_expr, irept::find(), symex_target_equationt::SSA_stept::guard, irept::id(), implied_guards(), irept::make_nil(), exprt::make_not(), exprt::make_true(), merge_identifier, merge_symbol, exprt::move_to_operands(), ns, exprt::operands(), read_trace(), symbol_exprt::set_identifier(), simplify(), size_type(), slice_SSA_steps(), sliced_guards, symex_target_equationt::SSA_stept::source, symex_target_equationt::SSA_stept::ssa_lhs, symex_target_equationt::SSA_steps, irept::swap(), t, and symex_target_equationt::SSA_stept::type.
Referenced by bmct::slice().
|
protected |
Definition at line 375 of file slice_by_trace.cpp.
References Forall_operands, irept::id(), exprt::is_true(), exprt::make_not(), ns, exprt::op1(), simplify(), symex_target_equationt::SSA_steps, and irept::swap().
Referenced by slice_by_trace().
|
protected |
Definition at line 33 of file slice_by_trace.h.
Referenced by compute_ts_back(), parse_alphabet(), parse_events(), and read_trace().
|
protected |
Definition at line 34 of file slice_by_trace.h.
Referenced by compute_ts_back(), parse_alphabet(), parse_events(), and read_trace().
|
protected |
Definition at line 56 of file slice_by_trace.h.
Referenced by slice_by_trace().
|
protected |
Definition at line 54 of file slice_by_trace.h.
Referenced by compute_ts_back(), and implied_guards().
|
protected |
Definition at line 52 of file slice_by_trace.h.
Referenced by assign_merges(), compute_ts_back(), and implied_guards().
|
protected |
Definition at line 58 of file slice_by_trace.h.
Referenced by assign_merges(), compute_ts_back(), and slice_by_trace().
|
protected |
Definition at line 31 of file slice_by_trace.h.
Referenced by compute_ts_back(), implied_guards(), implies_false(), slice_by_trace(), and slice_SSA_steps().
|
protected |
Definition at line 35 of file slice_by_trace.h.
Referenced by compute_ts_back(), and parse_alphabet().
|
protected |
Definition at line 40 of file slice_by_trace.h.
Referenced by compute_ts_back(), parse_events(), and read_trace().
|
protected |
Definition at line 44 of file slice_by_trace.h.
Referenced by compute_ts_back(), parse_events(), and read_trace().
|
protected |
Definition at line 50 of file slice_by_trace.h.
Referenced by compute_ts_back(), and slice_by_trace().
|
protected |
Definition at line 48 of file slice_by_trace.h.
Referenced by compute_ts_back(), read_trace(), and slice_by_trace().