build_goto_trace.cpp File Reference

#include <cassert>
#include <goto-symex/trace/build_goto_trace.h>
#include <goto-symex/state/renaming.h>
#include <goto-symex/witness/witnesses.h>
#include <solvers/smt/smt_conv.h>

Include dependency graph for build_goto_trace.cpp:

Functions
static bool	reads_through_dereference (const expr2tc &e)
expr2tc	build_lhs (smt_convt &smt_conv, const expr2tc &lhs)
expr2tc	build_rhs (smt_convt &smt_conv, const expr2tc &rhs)
static bool	is_model_value (const expr2tc &e)
static expr2tc	rebase_on_ssa_lhs (smt_convt &smt_conv, const expr2tc &lvalue, const expr2tc &ssa_lhs)
static expr2tc	build_component_value (smt_convt &smt_conv, const symex_target_equationt::SSA_stept &step)
static expr2tc	build_assignment_value (smt_convt &smt_conv, const symex_target_equationt::SSA_stept &step)
static expr2tc	nondet_read_value (smt_convt &smt_conv, const expr2tc &source, const expr2tc &renamed)
static void	collect_nondet_reads (smt_convt &smt_conv, const expr2tc &source, const expr2tc &renamed_in, std::list< std::pair< expr2tc, expr2tc > > &out)
static void	record_violated_reads (smt_convt &smt_conv, const expr2tc &ssa_cond, goto_trace_stept &step)
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)

Function Documentation

build_assignment_value()

expr2tc build_assignment_value ( smt_convt & smt_conv, const symex_target_equationt::SSA_stept & step )

static

build_component_value()

expr2tc build_component_value ( smt_convt & smt_conv, const symex_target_equationt::SSA_stept & step )

static

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 )

collect_nondet_reads()

void collect_nondet_reads ( smt_convt & smt_conv, const expr2tc & source, const expr2tc & renamed_in, std::list< std::pair< expr2tc, expr2tc > > & out )

static

is_model_value()

bool is_model_value ( const expr2tc & e )

static

nondet_read_value()

expr2tc nondet_read_value ( smt_convt & smt_conv, const expr2tc & source, const expr2tc & renamed )

static

reads_through_dereference()

bool reads_through_dereference ( const expr2tc & e )

static

rebase_on_ssa_lhs()

expr2tc rebase_on_ssa_lhs ( smt_convt & smt_conv, const expr2tc & lvalue, const expr2tc & ssa_lhs )

static

record_violated_reads()

void record_violated_reads ( smt_convt & smt_conv, const expr2tc & ssa_cond, goto_trace_stept & step )

static