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)
 
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, ssa_step_predicatet is_last_step_to_keep, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
 
void build_goto_trace (const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
 
static bool is_failed_assertion_step (symex_target_equationt::SSA_stepst::const_iterator step, const prop_convt &prop_conv)
 
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

◆ build_full_lhs_rec()

◆ build_goto_trace() [1/3]

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

◆ build_goto_trace() [2/3]

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

Definition at line 368 of file build_goto_trace.cpp.

References build_goto_trace().

◆ build_goto_trace() [3/3]

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

Definition at line 391 of file build_goto_trace.cpp.

References build_goto_trace(), and is_failed_assertion_step().

◆ is_failed_assertion_step()

static bool is_failed_assertion_step ( symex_target_equationt::SSA_stepst::const_iterator  step,
const prop_convt prop_conv 
)
static

Definition at line 384 of file build_goto_trace.cpp.

References tvt::is_false(), and prop_convt::l_get().

Referenced by build_goto_trace().

◆ set_internal_dynamic_object()

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 106 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().

◆ update_internal_field()

void update_internal_field ( const symex_target_equationt::SSA_stept SSA_step,
goto_trace_stept goto_trace_step,
const namespacet ns 
)