build_goto_trace.h File Reference

Traces of GOTO Programs. More...

#include "symex_target_equation.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 decision_proceduret &)>	ssa_step_predicatet

Functions
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. More...
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)
	Build a trace by going through the steps of target and stopping after the given step. More...
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)
	Build a trace by going through the steps of target and stopping after the step matching a given condition. More...

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 decision_proceduret &)> ssa_step_predicatet

Definition at line 48 of file build_goto_trace.h.

Function Documentation

build_goto_trace() [1/3]

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.

Parameters

	target	SSA form of the program
	decision_procedure	solver from which to get valuations
	ns	namespace
[out]	goto_trace	trace to which the steps of the trace get appended

Definition at line 452 of file build_goto_trace.cpp.

build_goto_trace() [2/3]

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
	)

Build a trace by going through the steps of target and stopping after the step matching a given condition.

Parameters

	target	SSA form of the program
	stop_after_predicate	function with an SSA step iterator and solver as argument, which should return true for the last step to keep
	decision_procedure	solver from which to get valuations
	ns	namespace
[out]	goto_trace	trace to which the steps of the trace get appended

Definition at line 207 of file build_goto_trace.cpp.

build_goto_trace() [3/3]

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
	)

Build a trace by going through the steps of target and stopping after the given step.

Parameters

	target	SSA form of the program
	last_step_to_keep	iterator pointing to the last step to keep
	decision_procedure	solver from which to get valuations
	ns	namespace
[out]	goto_trace	trace to which the steps of the trace get appended

Definition at line 428 of file build_goto_trace.cpp.