Stop assertion size-of-expr for pointer-checks

Since these can be void-pointers. In this case we simply skip introducing the
address-check altogether.

Author: petr-bauch

regression/cbmc/Void_Pointer_Init/main.c

@@ -0,0 +1,6 @@
+#include <assert.h>
+
+void foo(void *arg)
+{
+  assert(*(unsigned *)(arg) == 5);
+}

regression/cbmc/Void_Pointer_Init/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--function foo --pointer-check
+^\[foo.assertion.1\] line \d+ assertion \*\(unsigned \*\)\(arg\) == 5: FAILURE$
+^\[foo.pointer_dereference.4\] line \d+ dereference failure: dead object in \*\(\(unsigned int \*\)arg\): FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -1113,7 +1113,8 @@ void goto_checkt::pointer_validity_check(
   const exprt &pointer=expr.pointer();
 
   auto size_of_expr_opt = size_of_expr(expr.type(), ns);
-  CHECK_RETURN(size_of_expr_opt.has_value());
+  if(!size_of_expr_opt.has_value())
+    return; // in the case of `void*`
 
   auto conditions = address_check(pointer, size_of_expr_opt.value());