cbmc/build__goto__trace_8h_source.html

/*******************************************************************\


Module: Traces of GOTO Programs


Author: Daniel Kroening


Date: July 2005


\*******************************************************************/


#ifndef CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H

#define CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H


#include "symex_target_equation.h"


void build_goto_trace(

  const symex_target_equationt &target,

  const decision_proceduret &decision_procedure,

  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 decision_proceduret &decision_procedure,

  const namespacet &ns,

  goto_tracet &goto_trace);


typedef std::function<bool(

  symex_target_equationt::SSA_stepst::const_iterator,

  const decision_proceduret &)>

  ssa_step_predicatet;


void build_goto_trace(

  const symex_target_equationt &target,

  ssa_step_predicatet stop_after_predicate,

  const decision_proceduret &decision_procedure,

  const namespacet &ns,

  goto_tracet &goto_trace);


#endif // CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H

build_goto_trace
void build_goto_trace(const symex_target_equationt &target, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace)
Build a trace by going through the steps of target and stopping at the first failing assertion.
Definition build_goto_trace.cpp:452

ssa_step_predicatet
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const decision_proceduret &)> ssa_step_predicatet
Definition build_goto_trace.h:48

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

decision_proceduret
An interface for a decision procedure for satisfiability problems.
Definition decision_procedure.h:22

goto_tracet
Trace of a GOTO program.
Definition goto_trace.h:177

namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91

symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition symex_target_equation.h:34

symex_target_equation.h
Generate Equation using Symbolic Execution.