Traces of GOTO Programs. More...
#include "build_goto_trace.h"#include <util/arith_tools.h>#include <util/byte_operators.h>#include <util/namespace.h>#include <util/simplify_expr.h>#include <util/symbol.h>#include <goto-programs/goto_functions.h>#include <goto-programs/rewrite_union.h>#include <solvers/decision_procedure.h>#include "partial_order_concurrency.h"
Include dependency graph for build_goto_trace.cpp:Go to the source code of this file.
Functions | |
| static exprt | build_full_lhs_rec (const decision_proceduret &decision_procedure, const namespacet &ns, const exprt &src_original, const exprt &src_ssa) |
| static 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... | |
| static void | update_internal_field (const 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... | |
| static void | replace_nondet_in_type (typet &type, const decision_proceduret &solver) |
Replace nondet values that appear in type by their values as found by solver. More... | |
| static void | replace_nondet_in_type (exprt &expr, const decision_proceduret &solver) |
Replace nondet values that appear in the type of expr and its subexpressions type by their values as found by solver. More... | |
| void | build_goto_trace (const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace) |
Build a trace by going through the steps of target and stopping after the step matching a given condition. More... | |
| void | build_goto_trace (const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace) |
Build a trace by going through the steps of target and stopping after the given step. More... | |
| static bool | is_failed_assertion_step (symex_target_equationt::SSA_stepst::const_iterator step, const decision_proceduret &decision_procedure) |
| void | build_goto_trace (const symex_target_equationt &target, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace) |
Build a trace by going through the steps of target and stopping at the first failing assertion. More... | |
Detailed Description
Traces of GOTO Programs.
Definition in file build_goto_trace.cpp.
Function Documentation
◆ build_full_lhs_rec()
|
static |
Definition at line 29 of file build_goto_trace.cpp.
◆ build_goto_trace() [1/3]
| void build_goto_trace | ( | const symex_target_equationt & | target, |
| const decision_proceduret & | decision_procedure, | ||
| const namespacet & | ns, | ||
| goto_tracet & | goto_trace | ||
| ) |
Build a trace by going through the steps of target and stopping at the first failing assertion.
- Parameters
-
target SSA form of the program decision_procedure solver from which to get valuations ns namespace [out] goto_trace trace to which the steps of the trace get appended
Definition at line 452 of file build_goto_trace.cpp.
◆ build_goto_trace() [2/3]
| void build_goto_trace | ( | const symex_target_equationt & | target, |
| ssa_step_predicatet | stop_after_predicate, | ||
| const decision_proceduret & | decision_procedure, | ||
| const namespacet & | ns, | ||
| goto_tracet & | goto_trace | ||
| ) |
Build a trace by going through the steps of target and stopping after the step matching a given condition.
- Parameters
-
target SSA form of the program stop_after_predicate function with an SSA step iterator and solver as argument, which should return true for the last step to keep decision_procedure solver from which to get valuations ns namespace [out] goto_trace trace to which the steps of the trace get appended
Definition at line 207 of file build_goto_trace.cpp.
◆ build_goto_trace() [3/3]
| void build_goto_trace | ( | const symex_target_equationt & | target, |
| symex_target_equationt::SSA_stepst::const_iterator | last_step_to_keep, | ||
| const decision_proceduret & | decision_procedure, | ||
| const namespacet & | ns, | ||
| goto_tracet & | goto_trace | ||
| ) |
Build a trace by going through the steps of target and stopping after the given step.
- Parameters
-
target SSA form of the program last_step_to_keep iterator pointing to the last step to keep decision_procedure solver from which to get valuations ns namespace [out] goto_trace trace to which the steps of the trace get appended
Definition at line 428 of file build_goto_trace.cpp.
◆ is_failed_assertion_step()
|
static |
Definition at line 444 of file build_goto_trace.cpp.
◆ replace_nondet_in_type() [1/2]
|
static |
Replace nondet values that appear in the type of expr and its subexpressions type by their values as found by solver.
Definition at line 200 of file build_goto_trace.cpp.
◆ replace_nondet_in_type() [2/2]
|
static |
Replace nondet values that appear in type by their values as found by solver.
Definition at line 185 of file build_goto_trace.cpp.
◆ set_internal_dynamic_object()
|
static |
set internal field for variable assignment related to dynamic_object[0-9] and dynamic_[0-9]_array.
Definition at line 119 of file build_goto_trace.cpp.
◆ update_internal_field()
|
static |
set internal for variables assignments related to dynamic_object and CPROVER internal functions (e.g., __CPROVER_initialize)
Definition at line 148 of file build_goto_trace.cpp.
