Merge pull request #5793 from jezhiggins/vsd-value-set-implementation

Vsd value set implementation

Author: martin-cs

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
+--