Merge pull request #5825 from jezhiggins/vsd-value-set-of-pointers

Vsd value set of pointers

Author: martin-cs

regression/goto-analyzer/pointer-dereference-indeterminate-values/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main()
+{
+  int unknown;
+  int a = 10;
+
+  int *p = &a;
+
+  if(unknown)
+    a = 15;
+
+  int q = *p;
+
+  assert(q == a);
+}

regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-constants.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-values intervals --vsd-pointers constants
+^\[main.assertion.1\] line 15 assertion q == a: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-top-bottom.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-values intervals --vsd-pointers top-bottom
+^\[main.assertion.1\] line 15 assertion q == a: UNKNOWN
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-value-sets.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-values intervals --vsd-pointers value-set
+^\[main.assertion.1\] line 15 assertion q == a: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-dereference/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  int a = 10;
+  int *p = &a;
+
+  int q = *p;
+
+  assert(q == a);
+}

regression/goto-analyzer/pointer-dereference/test-constants.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-pointers constants
+^\[main.assertion.1\] line 10 assertion q == a: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-dereference/test-top-bottom.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-pointers top-bottom
+^\[main.assertion.1\] line 10 assertion q == a: UNKNOWN
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-dereference/test-value-sets.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-pointers value-set
+^\[main.assertion.1\] line 10 assertion q == a: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-write-through-indeterminate/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main()
+{
+  int unknown;
+  int a = 10;
+  int b = 10;
+  int *p = &a;
+
+  if(unknown)
+  {
+    b = 15;
+    *p = 15;
+  }
+
+  assert(*p == b);
+}

regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-constants.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-values intervals --vsd-pointers constants
+^\[main.assertion.1\] line 16 assertion \*p == b: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--