Make __CPROVER_allocated_memory work with non-POD type objects

The precision of local_bitvector_analysist is not sufficient to rule out several
cases introduced in 732ce2a.

Author: tautschnig

regression/cbmc/union12/main.c

@@ -0,0 +1,23 @@
+typedef struct
+{
+  union {
+    int access[256];
+  };
+} S1;
+
+typedef struct
+{
+  int c;
+} S2;
+
+static S1(*const l[1]) = {((S1 *)((0x50000000UL) + 0x00000))};
+
+void main()
+{
+  __CPROVER_allocated_memory(0x50000000UL, sizeof(S1));
+  l[0]->access[0] = 0;
+  __CPROVER_assert(l[0]->access[0] == 0, "holds");
+  __CPROVER_assert(l[0]->access[1] == 0, "should fail");
+  __CPROVER_allocated_memory(0x40000000UL + 0x40000, sizeof(S2));
+  ((S2 *)((0x40000000UL) + 0x40000))->c = 0x0707;
+}

regression/cbmc/union12/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.2\] line 20 should fail: FAILURE$
+^\*\* 1 of 17 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Despite the large array inside the union, the test should complete within 10
+seconds. Simplify extractbits(concatenation(...)) is essential to make this
+possible. With 77236cc34 (Avoid nesting of ID_with/byte_update by rewriting
+byte_extract to use the root object) the test already is trivial, however.

src/analyses/goto_check.cpp

@@ -1017,14 +1017,14 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
     if(flags.is_unknown() || flags.is_dynamic_heap())
     {
       conditions.push_back(conditiont(
-        not_exprt(deallocated(address, ns)),
+        or_exprt(allocs, not_exprt(deallocated(address, ns))),
         "deallocated dynamic object"));
     }
 
     if(flags.is_unknown() || flags.is_dynamic_local())
     {
       conditions.push_back(conditiont(
-        not_exprt(dead_object(address, ns)), "dead object"));
+        or_exprt(allocs, not_exprt(dead_object(address, ns))), "dead object"));
     }
 
     if(flags.is_unknown() || flags.is_dynamic_heap())
@@ -1034,7 +1034,10 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
         dynamic_object_upper_bound(address, ns, size));
 
       conditions.push_back(conditiont(
-        implies_exprt(malloc_object(address, ns), not_exprt(dynamic_bounds_violation)),
+        or_exprt(
+          allocs,
+          implies_exprt(
+            malloc_object(address, ns), not_exprt(dynamic_bounds_violation))),
         "pointer outside dynamic object bounds"));
     }
 
@@ -1047,7 +1050,11 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
         object_upper_bound(address, ns, size));
 
       conditions.push_back(conditiont(
-        implies_exprt(not_exprt(dynamic_object(address)), not_exprt(object_bounds_violation)),
+        or_exprt(
+          allocs,
+          implies_exprt(
+            not_exprt(dynamic_object(address)),
+            not_exprt(object_bounds_violation))),
         "pointer outside object bounds"));
     }