Merge pull request #6271 from jezhiggins/vsd-region-context

VSD - liveness context

Author: martin-cs

regression/goto-analyzer/liveness-array/main.c

@@ -0,0 +1,10 @@
+int main()
+{
+  int non_det;
+  int x[2] = {0, 1};
+
+  if(non_det)
+    x[0] = 2;
+  else
+    x[0] = 3;
+}

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

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-arrays every-element --vsd-values intervals --vsd-liveness --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::x .* TOP @ \[1\]
+^main::1::x .* \{\[0\] = \[0, 0\] @ \[2\]
+^main::1::x .* \{\[0\] = \[2, 3\] @ \[7\]
+--

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

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-arrays every-element --vsd-values intervals --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::x .* TOP @ \[1\]
+^main::1::x .* \{\[0\] = \[0, 0\] @ \[2\]
+^main::1::x .* \{\[0\] = \[2, 3\] @ \[4, 6\]
+--

regression/goto-analyzer/liveness-function-call/main.c

@@ -0,0 +1,22 @@
+int globalX;
+
+void f00()
+{
+}
+
+int main()
+{
+  globalX = 1;
+
+  f00();
+
+  assert(globalX == 1);
+
+  globalX = 2;
+
+  f00();
+
+  assert(globalX == 2);
+
+  return 0;
+}

regression/goto-analyzer/liveness-function-call/test-liveness-show.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-liveness --show
+^EXIT=0$
+^SIGNAL=0$
+globalX .* 0 @ \[28\]
+globalX .* 1 @ \[0\]
+globalX .* 2 @ \[3\]
+globalX .* TOP @ \[31\]
+--

regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-liveness --three-way-merge --show
+^EXIT=0$
+^SIGNAL=0$
+globalX .* 0 @ \[28\]
+globalX .* 1 @ \[0\]
+globalX .* 2 @ \[3\]
+globalX .* TOP @ \[31\]
+--

regression/goto-analyzer/liveness-function-call/test-liveness-three-way.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-liveness --three-way-merge --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .* globalX == 1: SUCCESS
+\[main.assertion.2\] .* globalX == 2: SUCCESS
+--

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

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-liveness --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .* globalX == 1: SUCCESS
+\[main.assertion.2\] .* globalX == 2: UNKNOWN
+--

regression/goto-analyzer/liveness-function-call/test-write-location-show.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --show
+^EXIT=0$
+^SIGNAL=0$
+globalX .* 0 @ \[28\]
+globalX .* 1 @ \[0\]
+globalX .* TOP @ \[0, 3\]
+--

regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --three-way-merge --show
+^EXIT=0$
+^SIGNAL=0$
+globalX .* 0 @ \[28\]
+globalX .* 1 @ \[0\]
+globalX .* 2 @ \[3\]
+--