array_set: do not fail upon an invalid (void) pointer

Even when the pointer cannot be successfully dereferenced, symex must
not yield an invariant failure.

Author: tautschnig

regression/cbmc/Array_operations3/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  void *p;
+  __CPROVER_array_set(p, 0);
+  __CPROVER_assert(
+    *(char *)p == 0, "should fail: array_set had no effect on invalid object");
+}

regression/cbmc/Array_operations3/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^\[main.assertion.1\] line 5 should fail: array_set had no effect on invalid object: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+An array_set on an invalid pointer must not result in an invariant failure.

src/goto-symex/symex_other.cpp

@@ -183,6 +183,11 @@ void goto_symext::symex_other(
     // obtain the actual array(s)
     process_array_expr(state, array_expr);
 
+    // if we dereferenced a void pointer, we may get a zero-sized (failed)
+    // object -- nothing to be assigned
+    if(array_expr.type().id() == ID_empty)
+      return;
+
     // prepare to build the array_of
     exprt value = clean_expr(code.op1(), state, false);