Merge pull request #4686 from tautschnig/fix-null-filtering

Fix value-set-based pointer test resolution for non-deterministic pointer values

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\[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,10 +1,8 @@
 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$
 --
-derefd_pointer::derefd_pointer
---
 See README for details about these tests

regression/cbmc/null5/main.c

@@ -0,0 +1,10 @@
+int *nondet_ptr();
+
+int main()
+{
+  int *ptr;
+  ptr = nondet_ptr();
+  if(ptr == 0)
+    return;
+  __CPROVER_assert(ptr != 0, "pointer cannot be null");
+}

regression/cbmc/null5/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Pull request #4444 introduced optimisations during symbolic execution that
+caused this test to spuriously fail (as the branch `ptr == 0` was removed).

src/pointer-analysis/value_set.cpp

@@ -976,9 +976,8 @@ void value_sett::get_value_set_rec(
   }
   else
   {
-    #if 0
-    std::cout << "WARNING: not doing " << expr.id() << '\n';
-    #endif
+    // for example: expr.id() == ID_nondet_symbol
+    insert(dest, exprt(ID_unknown, original_type));
   }
 
   #ifdef DEBUG