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.

Author: tautschnig

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
+main.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)
   {