Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_SYMEX_SLICE_BY_TRACE_H
13 #define CPROVER_GOTO_SYMEX_SLICE_BY_TRACE_H
27 std::string trace_files,
70 std::set<exprt> implications);
81 #endif // CPROVER_GOTO_SYMEX_SLICE_BY_TRACE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void compute_ts_back(symex_target_equationt &equation)
bool parse_alphabet(std::string read_line)
Base class for all expressions.
Expression to hold a symbol (variable)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
symbol_exprt merge_symbol
std::vector< std::pair< bool, std::set< exprt > > > merge_impl_cache_back
std::pair< std::set< irep_idt >, bool > event_sett
void assign_merges(symex_target_equationt &equation)
std::vector< event_sett > event_tracet
std::vector< exprt > trace_conditionst
std::vector< std::vector< irep_idt > > value_tracet
std::set< exprt > implied_guards(exprt e)
void read_trace(std::string filename)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
bool matches(event_sett s, irep_idt event)
std::set< irep_idt > alphabett
bool implies_false(exprt e)
void parse_events(std::string read_line)
std::set< exprt > sliced_guards
symex_slice_by_tracet(const namespacet &_ns)
irep_idt merge_identifier
void slice_SSA_steps(symex_target_equationt &equation, std::set< exprt > implications)
std::vector< exprt > merge_map_back