From 8a44e73b5e12a2ac8f8f2f59e7675cfe5ce690a1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 6 Jun 2019 15:56:05 +0000
Subject: [PATCH] Do not try to generate void objects

For void pointers (or structs containing void pointers) we cannot
generate "void" typed objects. Instead, generate char-typed objects as a
fall-back.
---
 .../generate-function-body-void/main.c         | 18 ++++++++++++++++++
 .../generate-function-body-void/test.desc      |  6 ++++++
 src/ansi-c/c_nondet_symbol_factory.cpp         |  8 ++++++--
 3 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 regression/goto-instrument/generate-function-body-void/main.c
 create mode 100644 regression/goto-instrument/generate-function-body-void/test.desc

diff --git a/regression/goto-instrument/generate-function-body-void/main.c b/regression/goto-instrument/generate-function-body-void/main.c
new file mode 100644
index 00000000000..d10dc8b2dc1
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-void/main.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+
+struct void_ptr
+{
+  void *ptr;
+};
+
+void havoc_struct(struct void_ptr *s);
+
+int main(void)
+{
+  struct void_ptr s;
+  havoc_struct(&s);
+  if(s.ptr)
+    *(char *)s.ptr = 42;
+  assert(!s.ptr || *(char *)s.ptr == 42);
+  return 0;
+}
diff --git a/regression/goto-instrument/generate-function-body-void/test.desc b/regression/goto-instrument/generate-function-body-void/test.desc
new file mode 100644
index 00000000000..ef395980918
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-void/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--generate-function-body 'havoc_struct' --generate-function-body-options 'havoc,params:.*'
+^VERIFICATION SUCCESSFUL$
+^SIGNAL=0$
+^EXIT=0$
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 08890749c92..5e91a9a2a73 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -71,8 +71,12 @@ void symbol_factoryt::gen_nondet_init(
 
     code_blockt non_null_inst;
 
-    exprt init_expr =
-      allocate_objects.allocate_object(non_null_inst, expr, subtype, lifetime);
+    typet object_type = subtype;
+    if(object_type.id() == ID_empty)
+      object_type = char_type();
+
+    exprt init_expr = allocate_objects.allocate_object(
+      non_null_inst, expr, object_type, lifetime);
 
     gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set, true);