build_goto_trace.h File Reference

#include <goto-symex/trace/goto_trace.h>
#include <goto-symex/equation/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.

Functions
void	build_goto_trace (const symex_target_equationt &target, smt_convt &smt_conv, goto_tracet &goto_trace)
void	build_successful_goto_trace (const symex_target_equationt &target, const namespacet &ns, goto_tracet &goto_trace)
expr2tc	build_lhs (smt_convt &smt_conv, const expr2tc &lhs)
expr2tc	build_rhs (smt_convt &smt_conv, const expr2tc &rhs)

Function Documentation

build_goto_trace()

void build_goto_trace	(	const symex_target_equationt &	target,
		smt_convt &	smt_conv,
		goto_tracet &	goto_trace )

build_lhs()

expr2tc build_lhs	(	smt_convt &	smt_conv,
		const expr2tc &	lhs )

build_rhs()

expr2tc build_rhs	(	smt_convt &	smt_conv,
		const expr2tc &	rhs )

build_successful_goto_trace()

void build_successful_goto_trace	(	const symex_target_equationt &	target,
		const namespacet &	ns,
		goto_tracet &	goto_trace )