cprover
|
Traces of GOTO Programs. More...
Go to the source code of this file.
Typedefs | |
typedef std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)> | ssa_step_predicatet |
Functions | |
void | build_goto_trace (const symex_target_equationt &target, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace) |
void | build_goto_trace (const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace) |
void | build_goto_trace (const symex_target_equationt &target, ssa_step_predicatet stop_after_predicate, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace) |
Traces of GOTO Programs.
Definition in file build_goto_trace.h.
typedef std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)> ssa_step_predicatet |
Definition at line 37 of file build_goto_trace.h.
void build_goto_trace | ( | const symex_target_equationt & | target, |
const prop_convt & | prop_conv, | ||
const namespacet & | ns, | ||
goto_tracet & | goto_trace | ||
) |
Definition at line 391 of file build_goto_trace.cpp.
References build_goto_trace(), and is_failed_assertion_step().
void build_goto_trace | ( | const symex_target_equationt & | target, |
symex_target_equationt::SSA_stepst::const_iterator | last_step_to_keep, | ||
const prop_convt & | prop_conv, | ||
const namespacet & | ns, | ||
goto_tracet & | goto_trace | ||
) |
Definition at line 368 of file build_goto_trace.cpp.
References build_goto_trace().
void build_goto_trace | ( | const symex_target_equationt & | target, |
ssa_step_predicatet | stop_after_predicate, | ||
const prop_convt & | prop_conv, | ||
const namespacet & | ns, | ||
goto_tracet & | goto_trace | ||
) |
Definition at line 165 of file build_goto_trace.cpp.
References goto_trace_stept::ACTUAL_PARAMETER, goto_trace_stept::assignment_type, symex_target_equationt::SSA_stept::assignment_type, build_full_lhs_rec(), goto_trace_stept::comment, goto_trace_stept::cond_expr, goto_trace_stept::cond_value, goto_trace_stept::format_string, goto_trace_stept::formatted, goto_trace_stept::full_lhs, goto_trace_stept::full_lhs_value, decision_proceduret::get(), symex_targett::GUARD, symex_target_equationt::SSA_stept::guard_literal, goto_trace_stept::hidden, symex_targett::HIDDEN_ACTUAL_PARAMETER, goto_trace_stept::identifier, INVARIANT, goto_trace_stept::io_args, goto_trace_stept::io_id, tvt::is_true(), prop_convt::l_get(), goto_trace_stept::lhs_object, goto_trace_stept::lhs_object_value, irept::make_nil(), goto_trace_stept::pc, symex_targett::PHI, partial_order_concurrencyt::rw_clock_id(), simplify(), symex_target_equationt::SSA_steps, goto_trace_stept::STATE, goto_trace_stept::step_nr, goto_tracet::steps, goto_trace_stept::thread_nr, to_integer(), goto_trace_stept::type, update_internal_field(), and symex_targett::VISIBLE_ACTUAL_PARAMETER.
Referenced by build_goto_trace(), bmct::error_trace(), bmc_all_propertiest::goal_covered(), fault_localizationt::goal_covered(), and bmc_covert::satisfying_assignment().