Prune TOP values in assume_eq

Found and fixed a problem in interval_abstract_value::to_constant(),
for case when interval is a valid single value, but the whole
thing is also top. This could arise in a merge of, say, [0, 0] and TOP.

Author: jezhiggins

regression/goto-analyzer/pruning-eq-nondet/main.c

@@ -0,0 +1,14 @@
+int main()
+{
+  int x = nondet();
+
+  if(x == 30)
+  {
+    assert(x == 20);
+    assert(x == 30);
+  }
+  else
+  {
+    assert(x != 30);
+  }
+}

regression/goto-analyzer/pruning-eq-nondet/test-constants.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x == 20: FAILURE
+\[main\.assertion\.2\] line .* assertion x == 30: SUCCESS
+\[main\.assertion\.3\] line .* assertion x != 30: UNKNOWN
+--

regression/goto-analyzer/pruning-eq-nondet/test-intervals.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x == 20: FAILURE
+\[main\.assertion\.2\] line .* assertion x == 30: SUCCESS
+\[main\.assertion\.3\] line .* assertion x != 30: UNKNOWN
+--

regression/goto-analyzer/pruning-eq-nondet/test-value-sets.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x == 20: FAILURE
+\[main\.assertion\.2\] line .* assertion x == 30: SUCCESS
+\[main\.assertion\.3\] line .* assertion x != 30: UNKNOWN
+--

regression/goto-analyzer/pruning-eq/main.c

@@ -0,0 +1,14 @@
+int main()
+{
+  int x = 0;
+  if(nondet())
+  {
+    x = 30;
+  }
+
+  if(x == 30)
+  {
+    assert(x == 20);
+    assert(x == 30);
+  }
+}

regression/goto-analyzer/pruning-eq/test-constants.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x == 20: FAILURE
+\[main\.assertion\.2\] line .* assertion x == 30: SUCCESS
+--

regression/goto-analyzer/pruning-eq/test-intervals.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x == 20: FAILURE
+\[main\.assertion\.2\] line .* assertion x == 30: SUCCESS
+--

regression/goto-analyzer/pruning-eq/test-value-sets.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x == 20: FAILURE
+\[main\.assertion\.2\] line .* assertion x == 30: SUCCESS
+--

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

@@ -0,0 +1,29 @@
+#include <assert.h>
+
+typedef int (*fptr_t)(int);
+
+int f(int x)
+{
+  return x + 1;
+}
+int g(int x)
+{
+  return x;
+}
+
+int main(void)
+{
+  int nondet_choice;
+
+  fptr_t fun2 = f;
+  if(nondet_choice)
+    fun2 = g;
+
+  fptr_t fun3;
+  if(nondet_choice)
+    fun3 = f;
+  else
+    fun3 = g;
+
+  return 0;
+}

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

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^main::1::fun2 \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end
+^main::1::fun3 \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end
+^EXIT=0$
+^SIGNAL=0$
+--