Vsd value set implementation

regression/goto-analyzer/ternary-operator/main.c

@@ -0,0 +1,19 @@
+#include <stdbool.h>
+
+extern int x;
+
+int main(void)
+{
+  bool b1;
+  bool b2;
+
+  b1 = true;
+  b2 = !b1;
+
+  bool b3 = x ? true : false;
+  int i = b1 ? 10 : 20;
+  int j = b2 ? 10 : 20;
+  int k = b3 ? 10 : 20;
+
+  return 0;
+}

regression/goto-analyzer/ternary-operator/test-constants.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::b1 \(\) -> TRUE @ \[2\]
+main::1::b2 \(\) -> FALSE @ \[3\]
+main::1::b3 \(\) -> TOP @ \[5\]
+main::1::i \(\) -> 10 @ \[7\]
+main::1::j \(\) -> 20 @ \[9\]
+main::1::k \(\) -> TOP @ \[11\]
+--

regression/goto-analyzer/ternary-operator/test-intervals.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values intervals --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::b1 \(\) -> \[1, 1\] @ \[2\]
+main::1::b2 \(\) -> \[0, 0\] @ \[3\]
+main::1::b3 \(\) -> \[0, 1\] @ \[5\]
+main::1::i \(\) -> \[A, A\] @ \[7\]
+main::1::j \(\) -> \[14, 14\] @ \[9\]
+main::1::k \(\) -> \[A, 14\] @ \[11\]
+--

regression/goto-analyzer/ternary-operator/test-value-sets.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::b1 \(\) -> value-set-begin: TRUE :value-set-end
+main::1::b2 \(\) -> value-set-begin: FALSE :value-set-end
+main::1::b3 \(\) -> value-set-begin: TRUE, FALSE :value-set-end
+main::1::i \(\) -> value-set-begin: 10 :value-set-end
+main::1::j \(\) -> value-set-begin: 20 :value-set-end
+main::1::k \(\) -> value-set-begin: 10, 20 :value-set-end
+--

regression/goto-analyzer/value-set-addition-01/main.c

@@ -0,0 +1,6 @@
+int main(int argc, char argv[])
+{
+  int p = 1;
+
+  int q = p + 2;
+}

regression/goto-analyzer/value-set-addition-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p .* value-set-begin: 1 :value-set-end
+main::1::q .* value-set-begin: 3 :value-set-end
+--

regression/goto-analyzer/value-set-addition-02/main.c

@@ -0,0 +1,7 @@
+int main(int argc, char argv[])
+{
+  int p = 2;
+  int q = 3;
+
+  int t = p + q;
+}

regression/goto-analyzer/value-set-addition-02/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p .* value-set-begin: 2 :value-set-end
+main::1::q .* value-set-begin: 3 :value-set-end
+main::1::t .* value-set-begin: 5 :value-set-end
+--

regression/goto-analyzer/value-set-addition-03/main.c

@@ -0,0 +1,11 @@
+int unknown();
+
+int main(int argc, char argv[])
+{
+  int p = 2;
+
+  if(unknown())
+    p += 2;
+  else
+    p += 3;
+}

regression/goto-analyzer/value-set-addition-03/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p .* value-set-begin: 4, 5 :value-set-end
+--

regression/goto-analyzer/value-set-addition-04/main.c

@@ -0,0 +1,14 @@
+int unknown();
+
+int main(int argc, char argv[])
+{
+  int p = 2;
+  int q = 3;
+
+  if(unknown())
+    p += 2;
+  else
+    p += 3;
+
+  int t = p + q;
+}

regression/goto-analyzer/value-set-addition-04/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p .* value-set-begin: 2 :value-set-end
+main::1::q .* value-set-begin: 3 :value-set-end
+main::1::p .* value-set-begin: 4, 5 :value-set-end
+main::1::t .* value-set-begin: 7, 8 :value-set-end
+--

regression/goto-analyzer/value-set-addition-05/main.c

@@ -0,0 +1,20 @@
+int unknown();
+
+int main(int argc, char argv[])
+{
+  int p;
+  int q;
+
+  if(unknown())
+  {
+    p = 2;
+    q = 5;
+  }
+  else
+  {
+    p = 3;
+    q = 10;
+  }
+
+  int t = p + q;
+}

regression/goto-analyzer/value-set-addition-05/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p .* value-set-begin: 2, 3 :value-set-end
+main::1::q .* value-set-begin: 5, 10 :value-set-end
+main::1::t .* value-set-begin: 7, 8, 12, 13 :value-set-end
+--

regression/goto-analyzer/value-set-addition-06/main.c

@@ -0,0 +1,21 @@
+int unknown();
+
+int main(int argc, char argv[])
+{
+  int p;
+  int q;
+  int r = 20;
+
+  if(unknown())
+  {
+    p = 2;
+    q = 5;
+  }
+  else
+  {
+    p = 3;
+    q = 10;
+  }
+
+  int t = p + q + r;
+}

regression/goto-analyzer/value-set-addition-06/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p .* value-set-begin: 2, 3 :value-set-end
+main::1::q .* value-set-begin: 5, 10 :value-set-end
+main::1::t .* value-set-begin: 27, 28, 32, 33 :value-set-end
+--

regression/goto-analyzer/value-set-addition-07/main.c

@@ -0,0 +1,23 @@
+int unknown();
+
+int main(int argc, char argv[])
+{
+  int p;
+  int q;
+  int r = 20;
+
+  if(unknown())
+    p = 2;
+  else
+    p = 3;
+  if(unknown())
+    q = 5;
+  else
+    q = 10;
+  if(unknown())
+    r = 20;
+  else
+    r = 30;
+
+  int t = p + q + r;
+}

regression/goto-analyzer/value-set-addition-07/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p .* value-set-begin: 2, 3 :value-set-end
+main::1::q .* value-set-begin: 5, 10 :value-set-end
+main::1::r .* value-set-begin: 20, 30 :value-set-end
+main::1::t .* value-set-begin: 27, 28, 32, 33, 37, 38, 42, 43 :value-set-end
+--

regression/goto-analyzer/value-set-addition-08/main.c

@@ -0,0 +1,22 @@
+int unknown();
+
+int main(int argc, char argv[])
+{
+  int p;
+  int q;
+  int r = 20;
+  ;
+
+  if(unknown())
+    p = 2;
+  else
+    p = 3;
+  if(unknown())
+    p = 4;
+  if(unknown())
+    q = 5;
+  else
+    q = 10;
+
+  int t = p + q + r;
+}

regression/goto-analyzer/value-set-addition-08/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p .* value-set-begin: 2, 3, 4 :value-set-end
+main::1::q .* value-set-begin: 5, 10 :value-set-end
+main::1::r .* value-set-begin: 20 :value-set-end
+main::1::t .* value-set-begin: 27, 28, 29, 32, 33, 34 :value-set-end
+--

regression/goto-analyzer/value-set-array-constant-access/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element
+^EXIT=0$
+^SIGNAL=0$
+main::1::second_value \(\) -> value-set-begin: 2 :value-set-end
+main::1::second_value_after_write \(\) -> value-set-begin: 10 :value-set-end

regression/goto-analyzer/value-set-convert-to-interval/main.c

@@ -0,0 +1,38 @@
+#include <stdbool.h>
+
+extern int x;
+
+int main(void)
+{
+  int a = 0;
+  int b = 20;
+  switch(x)
+  {
+  case 1:
+    a = 1;
+    b = 21;
+    break;
+  case 2:
+    a = 2;
+    b = 22;
+    break;
+  case 3:
+    a = 3;
+    b = 23;
+    break;
+  case 4:
+    a = 4;
+    b = 24;
+    break;
+  case 5:
+    a = 5;
+    break;
+  case 6:
+    a = 6;
+    break;
+  }
+
+  int c = a + b;
+
+  return 0;
+}

regression/goto-analyzer/value-set-convert-to-interval/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::a .* value-set-begin: 0, 1, 2, 3, 4, 5, 6 :value-set-end @ \[1, 12, 15, 18, 21, 24, 26\]
+main::1::b .* value-set-begin: 20, 21, 22, 23, 24 :value-set-end @ \[3, 13, 16, 19, 22\]
+main::1::c .* \[14, 1E\] @ \[30\]
+--

regression/goto-analyzer/value-set-function-pointers-arrays/test.desc

@@ -3,11 +3,11 @@ main.c
 --variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --show --pointer-check --three-way-merge
 ^file main.c line 29 function main: replacing function pointer by 2 possible targets$
 ^file main.c line 40 function main: replacing function pointer by 2 possible targets$
-^main::1::fun1 \(\) -> value-set-begin: ptr ->\([fg]\), ptr ->\([fg]\), :value-set-end$
-^main::1::fun_array3 \(\) -> \{\[0\] = value-set-begin: ptr ->\([fg]\), ptr ->\([fg]\), :value-set-end$
+^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end
+^main::1::fun_array3 \(\) -> \{\[0\] = value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^main::1::fun1 \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end$
-^main::1::fun_array3 \(\) -> \{\[0\] = value-set-begin: .*ptr ->\(h\).* :value-set-end$
+^main::1::fun1 \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end
+^main::1::fun_array3 \(\) -> \{\[0\] = value-set-begin: .*ptr ->\(h\).* :value-set-end

regression/goto-analyzer/value-set-function-pointers-incremented/test.desc → regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc

@@ -2,9 +2,8 @@ CORE
 main.c
 --variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check
 ^file main.c line 28 function main: replacing function pointer by 2 possible targets$
-^main::1::fun_incremented_show \(\) -> TOP$
+^main::1::fun_incremented_show \(\) -> value-set-begin: TOP :value-set-end
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^main::1::fun_incremented_show \(\) -> value-set-begin: .* :value-set-end$

regression/goto-analyzer/value-set-function-pointers-incremented-02/main.c

@@ -0,0 +1,34 @@
+#include <assert.h>
+
+typedef int (*fptr_t)(int);
+fptr_t fun_global, fun_global_show;
+
+int f(int x)
+{
+  return x + 1;
+}
+int g(int x)
+{
+  return x;
+}
+int h(int x)
+{
+  return x - 1;
+}
+
+int main(void)
+{
+  int i;
+  // This line is needed so that g is considered as a possibility for the TOP
+  // value
+  fptr_t dummy = g;
+
+  // function pointer incremented should be top
+  fptr_t fun_incremented = f;
+  if(i)
+    ++fun_incremented;
+  else
+    fun_incremented = h;
+  fun_incremented(5);
+  fptr_t fun_incremented_show = fun_incremented;
+}

regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check
+^file main.c line 32 function main: replacing function pointer by 3 possible targets$
+^main::1::fun_incremented_show \(\) -> value-set-begin: TOP, ptr ->\(h\) :value-set-end
+^EXIT=0$
+^SIGNAL=0$
+--