cprover
|
#include "build_goto_trace.h"
#include <cassert>
#include <util/arith_tools.h>
#include <util/byte_operators.h>
#include <util/simplify_expr.h>
#include <util/threeval.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) |
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) |
Traces of GOTO Programs
Definition in 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 28 of file build_goto_trace.cpp.
void build_goto_trace | ( | const symex_target_equationt & | target, |
const prop_convt & | prop_conv, | ||
const namespacet & | ns, | ||
goto_tracet & | goto_trace | ||
) |
Definition at line 389 of file build_goto_trace.cpp.
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 | ||
) |
Definition at line 166 of file build_goto_trace.cpp.
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 366 of file build_goto_trace.cpp.
|
static |
Definition at line 382 of file build_goto_trace.cpp.
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 107 of file build_goto_trace.cpp.
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 132 of file build_goto_trace.cpp.