CBMC
build_goto_trace.cpp File Reference

Traces of GOTO Programs. More...

+ 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 exprt build_full_lhs_rec ( const decision_proceduret decision_procedure,
const namespacet ns,
const exprt src_original,
const exprt src_ssa 
)
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
targetSSA form of the program
decision_proceduresolver from which to get valuations
nsnamespace
[out]goto_tracetrace 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
targetSSA form of the program
stop_after_predicatefunction with an SSA step iterator and solver as argument, which should return true for the last step to keep
decision_proceduresolver from which to get valuations
nsnamespace
[out]goto_tracetrace 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
targetSSA form of the program
last_step_to_keepiterator pointing to the last step to keep
decision_proceduresolver from which to get valuations
nsnamespace
[out]goto_tracetrace to which the steps of the trace get appended

Definition at line 428 of file build_goto_trace.cpp.

◆ is_failed_assertion_step()

static bool is_failed_assertion_step ( symex_target_equationt::SSA_stepst::const_iterator  step,
const decision_proceduret decision_procedure 
)
static

Definition at line 444 of file build_goto_trace.cpp.

◆ replace_nondet_in_type() [1/2]

static void replace_nondet_in_type ( exprt expr,
const decision_proceduret solver 
)
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 void replace_nondet_in_type ( typet type,
const decision_proceduret solver 
)
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 void set_internal_dynamic_object ( const exprt expr,
goto_trace_stept goto_trace_step,
const namespacet ns 
)
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 void update_internal_field ( const SSA_stept SSA_step,
goto_trace_stept goto_trace_step,
const namespacet ns 
)
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.