Skip to content

Commit f2abcec

Browse files
committed
introduce instructiont::turn_into_assume
This method turns a GOTO or an ASSERT instruction into an ASSUME with the same condition. This is a common pattern in the code base, and introducing the method enables doing so in a way that is guaranteed to preserve the class invariants.
1 parent e7eff1e commit f2abcec

File tree

6 files changed

+17
-8
lines changed

6 files changed

+17
-8
lines changed

src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -845,9 +845,7 @@ void disjunctive_polynomial_accelerationt::build_fixed()
845845
for(auto &instruction : fixed.instructions)
846846
{
847847
if(instruction.is_assert())
848-
{
849-
instruction.type = ASSUME;
850-
}
848+
instruction.turn_into_assume();
851849
}
852850

853851
// We're only interested in paths that loop back to the loop header.

src/goto-instrument/accelerate/sat_path_enumerator.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -196,7 +196,7 @@ void sat_path_enumeratort::build_fixed()
196196
for(auto &instruction : fixed.instructions)
197197
{
198198
if(instruction.is_assert())
199-
instruction.type = ASSUME;
199+
instruction.turn_into_assume();
200200
}
201201

202202
// We're only interested in paths that loop back to the loop header.

src/goto-instrument/contracts/contracts.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -261,8 +261,8 @@ void code_contractst::check_apply_loop_contracts(
261261
insert_before_swap_and_advance(goto_function.body, loop_end, havoc_code);
262262

263263
// change the back edge into assume(false) or assume(guard)
264-
loop_end->targets.clear();
265-
loop_end->type = ASSUME;
264+
loop_end->turn_into_assume();
265+
266266
if(loop_head->is_goto())
267267
loop_end->set_condition(false_exprt());
268268
else

src/goto-instrument/cover.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -311,7 +311,8 @@ static void instrument_cover_goals(
311311
{
312312
successor->turn_into_skip();
313313
}
314-
i_it->type = goto_program_instruction_typet::ASSUME;
314+
315+
i_it->turn_into_assume();
315316
}
316317
else
317318
{

src/goto-instrument/k_induction.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,7 @@ void k_inductiont::process_loop(
131131
{
132132
assert(t!=goto_function.body.instructions.end());
133133
if(t->is_assert())
134-
t->type=ASSUME;
134+
t->turn_into_assume();
135135
}
136136

137137
// assume the loop condition has become false

src/goto-programs/goto_program.h

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -441,6 +441,16 @@ class goto_programt
441441
clear(SKIP);
442442
}
443443

444+
/// Transforms either an assertion or a GOTO instruction
445+
/// into an assumption, with the same condition.
446+
void turn_into_assume()
447+
{
448+
PRECONDITION(_type == GOTO || _type == ASSERT);
449+
_type = ASSUME;
450+
targets.clear();
451+
code.make_nil();
452+
}
453+
444454
void complete_goto(targett _target)
445455
{
446456
PRECONDITION(type == INCOMPLETE_GOTO);

0 commit comments

Comments
 (0)