Skip to content

Commit 18700e0

Browse files
committed
Interpreter: remove unsupported target_assertion
The iterator was never initialised, but still being compared to, which is undefined behaviour.
1 parent 2a40de6 commit 18700e0

File tree

2 files changed

+9
-13
lines changed

2 files changed

+9
-13
lines changed

src/goto-programs/interpreter.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -742,9 +742,7 @@ void interpretert::execute_assert()
742742
{
743743
if(!evaluate_boolean(pc->get_condition()))
744744
{
745-
if((target_assert==pc) || stop_on_assertion)
746-
throw "program assertion reached";
747-
else if(show)
745+
if(show)
748746
error() << "assertion failed at " << pc->location_number
749747
<< "\n" << eom;
750748
}

src/goto-programs/interpreter_class.h

Lines changed: 8 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -30,14 +30,13 @@ class interpretert:public messaget
3030
interpretert(
3131
const symbol_tablet &_symbol_table,
3232
const goto_functionst &_goto_functions,
33-
message_handlert &_message_handler):
34-
messaget(_message_handler),
35-
symbol_table(_symbol_table),
36-
ns(_symbol_table),
37-
goto_functions(_goto_functions),
38-
stack_pointer(0),
39-
done(false),
40-
stop_on_assertion(false)
33+
message_handlert &_message_handler)
34+
: messaget(_message_handler),
35+
symbol_table(_symbol_table),
36+
ns(_symbol_table),
37+
goto_functions(_goto_functions),
38+
stack_pointer(0),
39+
done(false)
4140
{
4241
show=true;
4342
}
@@ -265,11 +264,10 @@ class interpretert:public messaget
265264
list_input_varst function_input_vars;
266265

267266
goto_functionst::function_mapt::const_iterator function;
268-
goto_programt::const_targett pc, next_pc, target_assert;
267+
goto_programt::const_targett pc, next_pc;
269268
goto_tracet steps;
270269
bool done;
271270
bool show;
272-
bool stop_on_assertion;
273271
static const size_t npos;
274272
size_t num_steps;
275273
size_t total_steps;

0 commit comments

Comments
 (0)