cprover
build_goto_trace.h File Reference

Traces of GOTO Programs. More...

Include dependency graph for build_goto_trace.h:
This graph shows which files directly or indirectly include this file:

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)
 

Detailed Description

Traces of GOTO Programs.

Definition in file build_goto_trace.h.

Typedef Documentation

◆ ssa_step_predicatet

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.

Function Documentation

◆ build_goto_trace() [1/3]

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().

◆ build_goto_trace() [2/3]

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().

◆ build_goto_trace() [3/3]

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 
)