Skip to content

Commit 39dd631

Browse files
committed
fixes
1 parent d2beb39 commit 39dd631

File tree

2 files changed

+8
-1
lines changed

2 files changed

+8
-1
lines changed

regression/goto-instrument-unwind/unwind-chain.sh

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ fi
1818
name=$(echo $2 | cut -d. -f1)
1919

2020
$goto_cc -o $name.gb $name.c
21+
$goto_instrument --show-goto-functions $name.gb
2122
$goto_instrument $1 $name.gb ${name}-unwound.gb
2223
$goto_instrument --show-goto-functions ${name}-unwound.gb
2324
$cbmc ${name}-unwound.gb

src/goto-instrument/unwind.cpp

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -176,10 +176,12 @@ void goto_unwindt::unwind(
176176
if(unwind_strategy==PARTIAL)
177177
{
178178
goto_programt::targett t=rest_program.add_instruction();
179+
unwind_log.insert(t, loop_head->location_number);
180+
179181
t->make_skip();
180182
t->source_location=loop_head->source_location;
181183
t->function=loop_head->function;
182-
unwind_log.insert(t, loop_head->location_number);
184+
t->location_number=loop_head->location_number;
183185
}
184186
else if(unwind_strategy==REST)
185187
{
@@ -216,6 +218,7 @@ void goto_unwindt::unwind(
216218

217219
new_t->source_location=loop_head->source_location;
218220
new_t->function=loop_head->function;
221+
new_t->location_number=loop_head->location_number;
219222
unwind_log.insert(new_t, loop_head->location_number);
220223
}
221224

@@ -242,6 +245,7 @@ void goto_unwindt::unwind(
242245
t_goto->source_location=loop_exit->source_location;
243246
t_goto->function=loop_exit->function;
244247
t_goto->guard=true_exprt();
248+
t_goto->location_number=loop_exit->location_number;
245249
}
246250

247251
// add a skip before the loop exit
@@ -252,6 +256,7 @@ void goto_unwindt::unwind(
252256
t_skip->make_skip();
253257
t_skip->source_location=loop_head->source_location;
254258
t_skip->function=loop_head->function;
259+
t_skip->location_number=loop_head->location_number;
255260

256261
// where to go for the next iteration
257262
goto_programt::targett loop_iter=t_skip;
@@ -293,6 +298,7 @@ void goto_unwindt::unwind(
293298
t_skip->make_skip();
294299
t_skip->source_location=loop_head->source_location;
295300
t_skip->function=loop_head->function;
301+
t_skip->location_number=loop_head->location_number;
296302

297303
// redirect gotos into loop body
298304
Forall_goto_program_instructions(i_it, goto_program)

0 commit comments

Comments
 (0)