From 199b2318757a93f185476a47253158e12664836f Mon Sep 17 00:00:00 2001
From: xbauch <petr.bauch@gmail.com>
Date: Mon, 22 Jul 2019 10:51:03 +0100
Subject: [PATCH 1/2] 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.
---
 regression/cbmc/Void_Pointer_Init/main.c    | 6 ++++++
 regression/cbmc/Void_Pointer_Init/test.desc | 9 +++++++++
 src/analyses/goto_check.cpp                 | 3 ++-
 3 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/Void_Pointer_Init/main.c
 create mode 100644 regression/cbmc/Void_Pointer_Init/test.desc

diff --git a/regression/cbmc/Void_Pointer_Init/main.c b/regression/cbmc/Void_Pointer_Init/main.c
new file mode 100644
index 00000000000..c9165c09ce7
--- /dev/null
+++ b/regression/cbmc/Void_Pointer_Init/main.c
@@ -0,0 +1,6 @@
+#include <assert.h>
+
+void foo(void *arg)
+{
+  assert(*(unsigned *)(arg) == 5);
+}
diff --git a/regression/cbmc/Void_Pointer_Init/test.desc b/regression/cbmc/Void_Pointer_Init/test.desc
new file mode 100644
index 00000000000..d39ab161cbf
--- /dev/null
+++ b/regression/cbmc/Void_Pointer_Init/test.desc
@@ -0,0 +1,9 @@
+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$
+--
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 7880faae78e..35ad6550cb6 100644
--- a/src/analyses/goto_check.cpp
+++ b/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());
 

From faf21d043517234fefeb58e9c61357e226d7af51 Mon Sep 17 00:00:00 2001
From: xbauch <petr.bauch@gmail.com>
Date: Mon, 22 Jul 2019 15:18:32 +0100
Subject: [PATCH 2/2] Implement converting void type

for the SMT2 queries.
---
 src/solvers/smt2/smt2_conv.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 1868627547a..c8a44618f49 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -2214,6 +2214,10 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
         convert_typecast(tmp);
       }
     }
+    else if(src_type.id() == ID_empty)
+    {
+      convert_expr(src);
+    }
     else
     {
       std::ostringstream e_str;
@@ -4626,6 +4630,11 @@ void smt2_convt::convert_type(const typet &type)
   {
     convert_type(c_bit_field_replacement_type(to_c_bit_field_type(type), ns));
   }
+  else if(type.id() == ID_empty)
+  {
+    // the NONDET(void) is in fact of type char
+    out << "(_ BitVec " << boolbv_width(char_type()) << " )";
+  }
   else
   {
     UNEXPECTEDCASE("unsupported type: "+type.id_string());