cprover
|
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"
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 | set_internal_dynamic_object (const exprt &expr, goto_trace_stept &goto_trace_step, const namespacet &ns) |
set internal field for variable assignment related to dynamic_object[0-9] and dynamic_[0-9]_array. More... | |
void | update_internal_field (const symex_target_equationt::SSA_stept &SSA_step, goto_trace_stept &goto_trace_step, const namespacet &ns) |
set internal for variables assignments related to dynamic_object and CPROVER internal functions (e.g., __CPROVER_initialize) More... | |
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) |
Traces of GOTO Programs.
Definition in file build_goto_trace.cpp.
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.
exprt build_full_lhs_rec | ( | const prop_convt & | prop_conv, |
const namespacet & | ns, | ||
const exprt & | src_original, | ||
const exprt & | src_ssa | ||
) |
Definition at line 27 of file build_goto_trace.cpp.
References index_exprt::array(), if_exprt::false_case(), decision_proceduret::get(), irept::id(), index_exprt::index(), irept::is_not_nil(), unary_exprt::op(), exprt::op0(), exprt::operands(), simplify(), member_exprt::struct_op(), to_if_expr(), to_index_expr(), to_member_expr(), to_typecast_expr(), and if_exprt::true_case().
Referenced by build_goto_trace().
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 173 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, 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, update_internal_field(), and symex_targett::VISIBLE_ACTUAL_PARAMETER.
Referenced by build_goto_trace(), bmct::error_trace(), bmc_all_propertiest::goal_covered(), fault_localizationt::goal_covered(), and bmc_covert::satisfying_assignment().
void build_goto_trace | ( | const symex_target_equationt & | target, |
const prop_convt & | prop_conv, | ||
const namespacet & | ns, | ||
goto_tracet & | goto_trace | ||
) |
Definition at line 352 of file build_goto_trace.cpp.
References build_goto_trace(), symex_target_equationt::SSA_steps, goto_tracet::steps, and goto_tracet::trim_after().
void set_internal_dynamic_object | ( | const exprt & | expr, |
goto_trace_stept & | goto_trace_step, | ||
const namespacet & | ns | ||
) |
set internal field for variable assignment related to dynamic_object[0-9] and dynamic_[0-9]_array.
Definition at line 114 of file build_goto_trace.cpp.
References forall_operands, irept::get_bool(), ssa_exprt::get_original_name(), irept::id(), goto_trace_stept::internal, namespacet::lookup(), to_ssa_expr(), and symbolt::type.
Referenced by update_internal_field().
void update_internal_field | ( | const symex_target_equationt::SSA_stept & | SSA_step, |
goto_trace_stept & | goto_trace_step, | ||
const namespacet & | ns | ||
) |
set internal for variables assignments related to dynamic_object and CPROVER internal functions (e.g., __CPROVER_initialize)
Definition at line 139 of file build_goto_trace.cpp.
References goto_functionst::entry_point(), goto_trace_stept::INPUT, goto_trace_stept::internal, symex_target_equationt::SSA_stept::is_function_call(), goto_trace_stept::OUTPUT, set_internal_dynamic_object(), symex_target_equationt::SSA_stept::source, symex_target_equationt::SSA_stept::ssa_lhs, symex_target_equationt::SSA_stept::ssa_rhs, and goto_trace_stept::type.
Referenced by build_goto_trace().