enable nondeterministic pointers

This commit enables the use of nondeterministic pointers, to allow
declarative modeling of states that include pointers.

Author: kroening

regression/cbmc/nondet-pointer/nondet-pointer1.c

@@ -0,0 +1,13 @@
+int *nondet_pointer();
+
+int main()
+{
+  int x = 123;
+  int *p = &x;
+  int *q = nondet_pointer();
+
+  if(p == q)
+    __CPROVER_assert(*q == 123, "value of *q");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer1.desc

@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/nondet-pointer/nondet-pointer2.c

@@ -0,0 +1,14 @@
+int *nondet_pointer();
+
+int main()
+{
+  int x = 123, y = 456;
+  int *px = &x;
+  int *py = &y;
+  int *q = nondet_pointer();
+
+  if(q == px || q == py)
+    __CPROVER_assert(*q == 123 || *q == 456, "value of *q");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer2.desc

@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/nondet-pointer/nondet-pointer3.c

@@ -0,0 +1,18 @@
+int *nondet_pointer();
+
+int main()
+{
+  int some_array[10];
+  int *p = some_array;
+  int *q = nondet_pointer();
+  int index;
+
+  __CPROVER_assume(index >= 0 && index < 10);
+  __CPROVER_assume(q == p);
+
+  q[index] = 123;
+
+  __CPROVER_assert(some_array[index] == 123, "value of array[index]");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer3.desc

@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/nondet-pointer/nondet-pointer4.c

@@ -0,0 +1,18 @@
+int *nondet_pointer();
+
+int main()
+{
+  int some_array[10];
+  int *p = some_array;
+  int *q = nondet_pointer();
+  int index;
+
+  __CPROVER_assume(index >= 0 && index < 10);
+  __CPROVER_assume(q == p + index);
+
+  *q = 123;
+
+  __CPROVER_assert(some_array[index] == 123, "value of array[index]");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer4.desc

@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/nondet-pointer/nondet-pointer5.c

@@ -0,0 +1,19 @@
+int *nondet_pointer();
+
+int main()
+{
+  int some_array[10];
+  int *p = some_array;
+  int *q = nondet_pointer();
+  int index;
+
+  __CPROVER_assume(index >= 0 && index < 10);
+  __CPROVER_assume(__CPROVER_same_object(p, q));
+  __CPROVER_assume(__CPROVER_POINTER_OFFSET(q) == sizeof(int) * index);
+
+  *q = 123;
+
+  __CPROVER_assert(some_array[index] == 123, "value of array[index]");
+
+  return 0;
+}

regression/cbmc/nondet-pointer/nondet-pointer5.desc

@@ -0,0 +1,8 @@
+CORE
+nondet-pointer1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/pointer-analysis/value_set.cpp

@@ -505,6 +505,23 @@ void value_sett::get_value_set_rec(
     else
       insert(dest, exprt(ID_unknown, original_type));
   }
+  else if(expr.id() == ID_nondet_symbol)
+  {
+    if(expr.type().id() == ID_pointer)
+    {
+      // we'll take the union of all objects we see, with unspecified offsets
+      values.iterate([this, &dest](const irep_idt &key, const entryt &value) {
+        for(const auto &object : value.object_map.read())
+          insert(dest, object.first, offsett());
+      });
+
+      // we'll add null, in case it's not there yet
+      insert(
+        dest,
+        exprt(ID_null_object, to_pointer_type(expr_type).subtype()),
+        offsett());
+    }
+  }
   else if(expr.id()==ID_if)
   {
     get_value_set_rec(
@@ -984,7 +1001,6 @@ void value_sett::get_value_set_rec(
   }
   else
   {
-    // for example: expr.id() == ID_nondet_symbol
     insert(dest, exprt(ID_unknown, original_type));
   }