Value sets must not return an empty set for nondet symbols

Even when the expression type is not immediately a pointer, some
component of the type may be a pointer. As such, it could legitimately
appear in pointer dereferencing, and we should at least add "unknown" to
the value set.

This is a follow-up fix to 3789670: the regression test included
yields a spurious counterexample in versions between 3789670 and this
bugfix commit. This commit also reverts the (spurious) changes to the
double_deref/* regression tests.

Author: tautschnig

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc

@@ -2,7 +2,7 @@ CORE
 double_deref_with_pointer_arithmetic.c
 --show-vcc
 ^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
-^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : main::argc!0@1#1 = 1
+^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc

@@ -1,7 +1,7 @@
 CORE
 double_deref_with_pointer_arithmetic_single_alias.c
 --show-vcc
-\{1\} main::argc!0@1#1 = 1
+\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object2\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/symex_should_exclude_null_pointers/nondet.c

@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+struct S
+{
+  int *p;
+  int x;
+};
+
+int main()
+{
+  struct S *s = malloc(sizeof(struct S));
+  // Guard must not be removed (deemed trivially true) by try_filter_value_sets.
+  if(s->p != NULL)
+    __CPROVER_assert(s->p != NULL, "cannot be NULL");
+}

regression/cbmc/symex_should_exclude_null_pointers/nondet.desc

@@ -0,0 +1,11 @@
+CORE
+nondet.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+try_filter_value_sets must not end up in a situation where it deems the guard
+trivially true. This situation arises when the value set wrongly is empty.

src/pointer-analysis/value_set.cpp

@@ -521,6 +521,8 @@ void value_sett::get_value_set_rec(
         exprt(ID_null_object, to_pointer_type(expr_type).subtype()),
         offsett());
     }
+    else
+      insert(dest, exprt(ID_unknown, original_type));
   }
   else if(expr.id()==ID_if)
   {