cprover
build_goto_trace.cpp File Reference

Traces of GOTO Programs. More...

#include "build_goto_trace.h"
#include <cassert>
#include <util/threeval.h>
#include <util/simplify_expr.h>
#include <util/arith_tools.h>
#include <solvers/prop/prop_conv.h>
#include <solvers/prop/prop.h>
#include "partial_order_concurrency.h"
Include dependency graph for build_goto_trace.cpp:

Go to the source code of this file.

Functions

exprt build_full_lhs_rec (const prop_convt &prop_conv, const namespacet &ns, const exprt &src_original, const exprt &src_ssa)
 
exprt adjust_lhs_object (const prop_convt &prop_conv, const namespacet &ns, const exprt &src)
 
void build_goto_trace (const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator end_step, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
 
void build_goto_trace (const symex_target_equationt &target, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
 

Detailed Description

Traces of GOTO Programs.

Definition in file build_goto_trace.cpp.

Function Documentation

§ adjust_lhs_object()

exprt adjust_lhs_object ( const prop_convt prop_conv,
const namespacet ns,
const exprt src 
)

Definition at line 104 of file build_goto_trace.cpp.

§ build_full_lhs_rec()

§ build_goto_trace() [1/2]

void build_goto_trace ( const symex_target_equationt target,
symex_target_equationt::SSA_stepst::const_iterator  end_step,
const prop_convt prop_conv,
const namespacet ns,
goto_tracet goto_trace 
)

Definition at line 112 of file build_goto_trace.cpp.

References goto_trace_stept::ACTUAL_PARAMETER, goto_trace_stept::assignment_type, symex_target_equationt::SSA_stept::assignment_type, build_full_lhs_rec(), goto_trace_stept::comment, symex_target_equationt::SSA_stept::comment, goto_trace_stept::cond_expr, symex_target_equationt::SSA_stept::cond_expr, symex_target_equationt::SSA_stept::cond_literal, goto_trace_stept::cond_value, symex_target_equationt::SSA_stept::converted_io_args, current_time(), goto_trace_stept::format_string, symex_target_equationt::SSA_stept::format_string, goto_trace_stept::formatted, symex_target_equationt::SSA_stept::formatted, goto_trace_stept::full_lhs, goto_trace_stept::full_lhs_value, decision_proceduret::get(), ssa_exprt::get_original_expr(), symex_targett::GUARD, symex_target_equationt::SSA_stept::guard_literal, goto_trace_stept::hidden, symex_target_equationt::SSA_stept::hidden, symex_targett::HIDDEN_ACTUAL_PARAMETER, goto_trace_stept::identifier, symex_target_equationt::SSA_stept::identifier, goto_trace_stept::io_args, goto_trace_stept::io_id, symex_target_equationt::SSA_stept::io_id, symex_target_equationt::SSA_stept::is_assert(), symex_target_equationt::SSA_stept::is_assume(), symex_target_equationt::SSA_stept::is_goto(), irept::is_not_nil(), tvt::is_true(), prop_convt::l_get(), goto_trace_stept::lhs_object, goto_trace_stept::lhs_object_value, irept::make_nil(), symex_target_equationt::SSA_stept::original_full_lhs, goto_trace_stept::pc, symex_targett::PHI, partial_order_concurrencyt::rw_clock_id(), simplify(), symex_target_equationt::SSA_stept::source, symex_target_equationt::SSA_stept::ssa_full_lhs, symex_target_equationt::SSA_stept::ssa_lhs, symex_target_equationt::SSA_steps, goto_trace_stept::STATE, goto_tracet::steps, goto_trace_stept::thread_nr, to_integer(), goto_tracet::trim_after(), goto_trace_stept::type, symex_target_equationt::SSA_stept::type, and symex_targett::VISIBLE_ACTUAL_PARAMETER.

Referenced by build_goto_trace(), path_searcht::check_assertion(), bmct::error_trace(), bmc_all_propertiest::goal_covered(), fault_localizationt::goal_covered(), and bmc_covert::satisfying_assignment().

§ build_goto_trace() [2/2]

void build_goto_trace ( const symex_target_equationt target,
const prop_convt prop_conv,
const namespacet ns,
goto_tracet goto_trace 
)