Skip to content

Commit 3f5cfb8

Browse files
committed
Enable remove_skip to soundly remove skips with labels
1 parent f69c71d commit 3f5cfb8

File tree

2 files changed

+9
-3
lines changed

2 files changed

+9
-3
lines changed

src/goto-programs/remove_skip.cpp

+5-2
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,10 @@ Author: Daniel Kroening, [email protected]
1212
#include "remove_skip.h"
1313
#include "goto_model.h"
1414

15-
bool is_skip(const goto_programt &body, goto_programt::const_targett it)
15+
bool is_skip(
16+
const goto_programt &body,
17+
goto_programt::const_targett it,
18+
bool ignore_labels)
1619
{
1720
// we won't remove labelled statements
1821
// (think about error labels or the like)
@@ -100,7 +103,7 @@ void remove_skip(
100103
// for collecting labels
101104
std::list<irep_idt> labels;
102105

103-
while(is_skip(goto_program, it))
106+
while(is_skip(goto_program, it, true))
104107
{
105108
// don't remove the last skip statement,
106109
// it could be a target

src/goto-programs/remove_skip.h

+4-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,10 @@ Author: Daniel Kroening, [email protected]
1616

1717
class goto_modelt;
1818

19-
bool is_skip(const goto_programt &, goto_programt::const_targett);
19+
bool is_skip(
20+
const goto_programt &,
21+
goto_programt::const_targett,
22+
bool ignore_labels = false);
2023
void remove_skip(goto_programt &);
2124
void remove_skip(goto_functionst &);
2225
void remove_skip(goto_modelt &);

0 commit comments

Comments
 (0)