Skip to content

Commit 6f7c25f

Browse files
committed
Swapping goto_programt::instructiont must preserve labels
The swap method should maintain all information that cannot be computed. (As those are computed, instruction numbers, incoming edges, target numbers, loop numbers need not be preserved.)
1 parent 718b547 commit 6f7c25f

File tree

3 files changed

+49
-0
lines changed

3 files changed

+49
-0
lines changed
Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
int foo()
5+
{
6+
return 1;
7+
}
8+
9+
typedef int (*fptr_t)(void);
10+
11+
int main()
12+
{
13+
label_zero:
14+
assert(1);
15+
int x;
16+
int *p;
17+
goto label_two;
18+
label_one:
19+
assert(x < 0 || x >= 0);
20+
label_two:
21+
p = malloc(sizeof(int));
22+
label_three:
23+
if(foo())
24+
x = 42;
25+
label_four:
26+
assert(foo() == 1);
27+
label_five:
28+
fptr_t fp = foo;
29+
assert(fp() == 1);
30+
label_six:
31+
return *p;
32+
}
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
4+
Labels: label_zero$
5+
Labels: label_one$
6+
Labels: label_two$
7+
Labels: label_three$
8+
Labels: label_four$
9+
Labels: label_five$
10+
Labels: label_six$
11+
^EXIT=0$
12+
^SIGNAL=0$
13+
--
14+
^warning: ignoring
15+
--
16+
This test ensures that label names specified in the source code are preserved.

src/goto-programs/goto_program.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -527,6 +527,7 @@ class goto_programt
527527
swap(instruction._type, _type);
528528
swap(instruction.guard, guard);
529529
swap(instruction.targets, targets);
530+
swap(instruction.labels, labels);
530531
}
531532

532533
/// Uniquely identify an invalid target or location

0 commit comments

Comments
 (0)