Skip to content

Commit 3761704

Browse files
author
Daniel Kroening
committed
avoid access to instructiont::code
1 parent 9a5345e commit 3761704

File tree

3 files changed

+3
-4
lines changed

3 files changed

+3
-4
lines changed

src/goto-symex/build_goto_trace.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,7 @@ static void update_internal_field(
161161
// "__CPROVER_*" function calls in __CPROVER_start are already marked as
162162
// internal. Don't mark any other function calls (i.e. "main"), function
163163
// arguments or any other parts of a code_function_callt as internal.
164-
if(SSA_step.source.pc->code.get_statement()!=ID_function_call)
164+
if(!SSA_step.is_function_call())
165165
goto_trace_step.internal=true;
166166
}
167167
}

src/goto-symex/memory_model_tso.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ void memory_model_tsot::program_order(
106106

107107
if((*e_it2)->is_memory_barrier())
108108
{
109-
const codet &code = (*e_it2)->source.pc->code;
109+
const codet &code = (*e_it2)->source.pc->get_other();
110110

111111
if((*e_it)->is_shared_read() &&
112112
!code.get_bool(ID_RRfence) &&

src/goto-symex/symex_goto.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -122,8 +122,7 @@ void goto_symext::symex_goto(statet &state)
122122
{
123123
DATA_INVARIANT(
124124
instruction.targets.size() > 0,
125-
"Instruction is an unconditional goto with no target: " +
126-
instruction.code.pretty());
125+
"Instruction is an unconditional goto with no target");
127126
symex_transition(state, instruction.get_target(), true);
128127
return;
129128
}

0 commit comments

Comments
 (0)