build_goto_trace.h File Reference

Traces of GOTO Programs. More...

#include "symex_target_equation.h"
#include "goto_symex_state.h"

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 389 of file build_goto_trace.cpp.

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
	)

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
	)

Definition at line 166 of file build_goto_trace.cpp.