Merge pull request #4759 from tautschnig/no-init-void

Do not try to generate void objects

Author: Daniel Kroening

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;
+}

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$

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);