Skip to content

Commit 24b0721

Browse files
committed
Further liveness regression tests
1 parent 5ea6df5 commit 24b0721

File tree

9 files changed

+71
-2
lines changed

9 files changed

+71
-2
lines changed
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int main()
2+
{
3+
int non_det;
4+
int x = 0;
5+
6+
for(int i = 0; i != 5; ++i)
7+
{
8+
int y = 0;
9+
x++;
10+
y = 1;
11+
}
12+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --vsd-liveness --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
8+
^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[9\]
9+
^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[5\]
10+
--
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
8+
^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[8\]
9+
^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[2, 8\]
10+
--
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
int main()
2+
{
3+
int non_det;
4+
int x = 0;
5+
int *p = &x;
6+
7+
if(non_det)
8+
*p = 2;
9+
else
10+
*p = 3;
11+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --vsd-pointers constants --vsd-liveness --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
8+
^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[9\]
9+
^main::1::p .* TOP @ \[3\]
10+
^main::1::p .*\(main::1::x\) @ \[4\]
11+
--
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --vsd-pointers constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
8+
^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[6, 8\]
9+
^main::1::p .* TOP @ \[3\]
10+
^main::1::p .*\(main::1::x\) @ \[4\]
11+
--

regression/goto-analyzer/liveness/test-liveness.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,7 @@ main.c
33
--variable-sensitivity --vsd-values set-of-constants --vsd-liveness --show
44
^EXIT=0$
55
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
68
^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[7\]
79
--

regression/goto-analyzer/liveness/test-write-location.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,7 @@ main.c
33
--variable-sensitivity --vsd-values set-of-constants --show
44
^EXIT=0$
55
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
68
^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[4, 6\]
79
--

src/analyses/variable-sensitivity/liveness_context.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010

1111
abstract_objectt::locationt liveness_contextt::get_location() const
1212
{
13-
return *assign_location;
13+
return assign_location.has_value() ? assign_location.value() : locationt();
1414
}
1515

1616
/**
@@ -164,7 +164,7 @@ void liveness_contextt::output(
164164
if(assign_location.has_value())
165165
out << " @ [" << assign_location.value()->location_number << "]";
166166
else
167-
out << " @ [merge-point]";
167+
out << " @ [undefined]";
168168
}
169169

170170
/**

0 commit comments

Comments
 (0)