Skip to content

Commit a20bff7

Browse files
committed
Fix a bug in slice global inits where guard expressions were disregarded
1 parent 7e00a30 commit a20bff7

File tree

5 files changed

+44
-0
lines changed

5 files changed

+44
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
2+
int x;
3+
int y;
4+
5+
int main()
6+
{
7+
if (x) {
8+
y = 1;
9+
}
10+
11+
return 0;
12+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--slice-global-inits
4+
x = 0;$
5+
y = 0;$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
2+
int x;
3+
int y;
4+
5+
void func(int a, int b) {}
6+
7+
int main()
8+
{
9+
func(x, y);
10+
11+
return 0;
12+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--slice-global-inits
4+
x = 0;$
5+
y = 0;$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring

src/goto-programs/slice_global_inits.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,8 @@ void slice_global_inits(goto_modelt &goto_model)
7777
{
7878
const codet &code=i_it->code;
7979
code.visit(visitor);
80+
const exprt &expr=i_it->guard;
81+
expr.visit(visitor);
8082
}
8183
}
8284

0 commit comments

Comments
 (0)