Merge pull request #6023 from jezhiggins/vsd-widening-implementation

Vsd meet and assume

Author: martin-cs

regression/goto-analyzer/branching-ge/main-always.c

@@ -0,0 +1,17 @@
+int unknown();
+
+int main()
+{
+  int i = 0;
+  int p = 0;
+
+  if(unknown())
+    p = 5;
+  if(unknown())
+    p = 10;
+
+  if(p >= 0)
+    i = 5;
+  else
+    i = -5;
+}

regression/goto-analyzer/branching-ge/main-indeterminate.c

@@ -0,0 +1,17 @@
+int unknown();
+
+int main()
+{
+  int i = 0;
+  int p = 0;
+
+  if(unknown())
+    p = 5;
+  if(unknown())
+    p = 10;
+
+  if(p >= 5)
+    i = 5;
+  else
+    i = -5;
+}

regression/goto-analyzer/branching-ge/main-never.c

@@ -0,0 +1,17 @@
+int unknown();
+
+int main()
+{
+  int i = 0;
+  int p = 0;
+
+  if(unknown())
+    p = 5;
+  if(unknown())
+    p = 10;
+
+  if(p >= 11)
+    i = 5;
+  else
+    i = -5;
+}

regression/goto-analyzer/branching-ge/test-always-constants.desc

@@ -0,0 +1,8 @@
+CORE
+main-always.c
+--variable-sensitivity --vsd-values constants --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::i .* TOP @ \[17, 19\]
+^main::1::p .* TOP @ \[3, 8, 14\]
+--

regression/goto-analyzer/branching-ge/test-always-intervals.desc

@@ -0,0 +1,8 @@
+CORE
+main-always.c
+--variable-sensitivity --vsd-values intervals --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::i .* \[5, 5\] @ \[17\]
+^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+--

regression/goto-analyzer/branching-ge/test-always-value-set.desc

@@ -0,0 +1,8 @@
+CORE
+main-always.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+--

regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc

@@ -0,0 +1,8 @@
+CORE
+main-indeterminate.c
+--variable-sensitivity --vsd-values constants --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::i .* TOP @ \[17, 19\]
+^main::1::p .* TOP @ \[3, 8, 14\]
+--

regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc

@@ -0,0 +1,8 @@
+CORE
+main-indeterminate.c
+--variable-sensitivity --vsd-values intervals --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\]
+^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+--

regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc

@@ -0,0 +1,8 @@
+CORE
+main-indeterminate.c
+--variable-sensitivity --vsd-values set-of-constants --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+--

regression/goto-analyzer/branching-ge/test-never-constants.desc

@@ -0,0 +1,8 @@
+CORE
+main-never.c
+--variable-sensitivity --vsd-values constants --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::i .* TOP @ \[17, 19\]
+^main::1::p .* TOP @ \[3, 8, 14\]
+--