heap allocation and value-set tests

Author: jezhiggins

regression/goto-analyzer/heap-allocation-nondet-1/main.c

@@ -0,0 +1,9 @@
+
+int main() {
+  int* q = malloc(10);
+  int* r = malloc(10);
+
+  int *p = r;
+  if (nondet())
+    p = q;
+}

regression/goto-analyzer/heap-allocation-nondet-1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-1\[0\]\) :value-set-end
+--

regression/goto-analyzer/heap-allocation-nondet-2/main.c

@@ -0,0 +1,6 @@
+
+int main() {
+  int *p = malloc(10);
+  if (nondet())
+    ++p;
+}

regression/goto-analyzer/heap-allocation-nondet-2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-0\[1\]\) :value-set-end
+--

regression/goto-analyzer/heap-allocation-nondet-3/main.c

@@ -0,0 +1,9 @@
+
+int main() {
+  int *q = malloc(10);
+  int r[10];
+
+  int *p = r;
+  if (nondet())
+    p = q;
+}

regression/goto-analyzer/heap-allocation-nondet-3/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(main::1::r\[0\]\), ptr ->\(heap-allocation-0\[0\]\) :value-set-end
+--

regression/goto-analyzer/heap-allocation-nondet-4/main.c

@@ -0,0 +1,9 @@
+
+int main() {
+  int *q = malloc(10);
+  int r[10];
+
+  int *p = q;
+  if (nondet())
+    p = r;
+}

regression/goto-analyzer/heap-allocation-nondet-4/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(main::1::r\[0\]\), ptr ->\(heap-allocation-0\[0\]\) :value-set-end
+--