Merge pull request #3419 from tautschnig/void-deref

Remove unnecessary assertion about using 0-size objects

Author: tautschnig

regression/cbmc/void_pointer4/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+struct S
+{
+  int a;
+};
+
+void foo(struct S *x)
+{
+  x->a = 42;
+  assert(x->a == 42);
+}
+
+int main()
+{
+  void *p;
+  foo(p);
+}

regression/cbmc/void_pointer4/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

scripts/delete_failing_smt2_solver_tests

@@ -192,4 +192,5 @@ rm union9/test.desc
 rm unsigned___int128/test.desc
 rm void_pointer2/test.desc
 rm void_pointer3/test.desc
+rm void_pointer4/test.desc
 rm while1/test.desc

src/util/std_expr.cpp

@@ -131,8 +131,6 @@ void object_descriptor_exprt::build(
     offset()=from_integer(0, index_type());
 
   build_object_descriptor_rec(ns, expr, *this);
-
-  POSTCONDITION(root_object().type().id() != ID_empty);
 }
 
 shift_exprt::shift_exprt(