Allow (possibly nested) pointers to be dereferenced to void

Author: svorenova

src/pointer-analysis/value_set_dereference.cpp

@@ -201,13 +201,23 @@ bool value_set_dereferencet::dereference_type_compare(
   const typet &object_type,
   const typet &dereference_type) const
 {
-  if(dereference_type.id()==ID_empty)
-    return true; // always ok (anything can be dereferenced to void type)
-
-  if(
-    object_type.id() == ID_pointer && dereference_type.id() == ID_pointer &&
-    dereference_type.subtype().id() == ID_empty)
-    return true; // also ok (any pointer can be dereferenced to a void pointer)
+  // check if the two types have matching number of ID_pointer levels, with
+  // the dereference type eventually pointing to void; then this is ok
+  // for example:
+  // - dereference_type=void is ok (no matter what object_type is);
+  // - object_type=(int *), dereference_type=(void *) is ok;
+  // - object_type=(int **), dereference_type=(void **) is ok;
+  // - object_type=(int *), dereference_type=(void **) is not ok;
+  typet object_unwrapped = object_type;
+  typet dereference_unwrapped = dereference_type;
+  while(object_unwrapped.id() == ID_pointer &&
+        dereference_unwrapped.id() == ID_pointer)
+  {
+    object_unwrapped = object_unwrapped.subtype();
+    dereference_unwrapped = dereference_unwrapped.subtype();
+  }
+  if(dereference_unwrapped.id() == ID_empty)
+    return true;
 
   if(base_type_eq(object_type, dereference_type, ns))
     return true; // ok, they just match