Add a test for the value set analysis in goto-instrument

Previously there were no direct checks for this functionality, only for
users such as the memory model functionality.

Author: martin

regression/goto-instrument/show-value-sets/main.c

@@ -0,0 +1,41 @@
+#include <stdlib.h>
+
+#define BIG 4096
+
+int main()
+{
+  // Uninitialized pointer
+  int *u;
+
+  // Basic assignment
+  u = NULL;
+  int a;
+  u = &a;
+
+  // Test merging and the loss of correlation
+  int *p;
+  int *q;
+  int b;
+  int c;
+  int nondet;
+  if(nondet)
+  {
+    p = &b;
+    q = &c;
+  }
+  else
+  {
+    p = &c;
+    q = &b;
+  }
+
+  // Test widening
+  int array[BIG];
+  int *s = &(array[0]);
+  for(int i = 0; i < BIG; ++i)
+  {
+    s = &array[i];
+  }
+
+  return 0;
+}

regression/goto-instrument/show-value-sets/test.desc

@@ -0,0 +1,27 @@
+CORE
+main.c
+--show-value-sets
+^EXIT=0$
+^SIGNAL=0$
+main::1::u = \{ <main::1::u\$object, 0, signedbv\[32\]> \}
+main::1::u = \{ <NULL-object, 0, signedbv\[32\]> \}
+main::1::u = \{ <main::1::a, 0, signedbv\[32\]> \}
+main::1::p = \{ <main::1::b, 0, signedbv\[32\]> \}
+main::1::p = \{ <main::1::c, 0, signedbv\[32\]> \}
+main::1::q = \{ <main::1::b, 0, signedbv\[32\]>, <main::1::c, 0, signedbv\[32\]> \}
+main::1::p = \{ <main::1::b, 0, signedbv\[32\]>, <main::1::c, 0, signedbv\[32\]> \}
+main::1::s = \{ <main::1::array\[0\], \*, signedbv\[32\]> \}
+--
+--
+A few basic tests to check if value sets are being handled correctly.
+
+It would be reasonable to ask about the checks for:
+
+main::1::q = \{ <main::1::b, 0, signedbv\[32\]> \}
+main::1::q = \{ <main::1::c, 0, signedbv\[32\]> \}
+
+but as domains are stored at the start of instructions the following merge will
+over-write it on one branch or the other.  To keep the test portable it is best
+avoided.
+
+