Take __CPROVER_allocated_memory regions into account for --bounds-check

regression/cbmc/memory_allocation2/main.c

@@ -0,0 +1,39 @@
+#define _cbmc_printf2(str, var)                                                \
+  {                                                                            \
+    unsigned int ValueOf_##str = (unsigned int)var;                            \
+  }
+
+#define BUFFER_SIZE 100
+typedef struct
+{
+  int buffer[BUFFER_SIZE];
+} buffert;
+
+#define BUF_BASE 0x1000
+#define BUF0_BASE (BUF_BASE + 0x00000)
+#define BUF1_BASE (BUF_BASE + 0x10000)
+#define BUF2_BASE (BUF_BASE + 0x20000)
+#define BUF3_BASE (BUF_BASE + 0x30000)
+
+#define BUF0 ((buffert *)BUF0_BASE)
+#define BUF1 ((buffert *)BUF1_BASE)
+#define BUF2 ((buffert *)BUF2_BASE)
+#define BUF3 ((buffert *)BUF3_BASE)
+
+static buffert(*const buffers[4]) = {BUF0, BUF1, BUF2, BUF3};
+
+main()
+{
+  __CPROVER_allocated_memory(BUF0_BASE, sizeof(buffert));
+  __CPROVER_allocated_memory(BUF1_BASE, sizeof(buffert));
+  __CPROVER_allocated_memory(BUF2_BASE, sizeof(buffert));
+  __CPROVER_allocated_memory(BUF3_BASE, sizeof(buffert));
+
+  _cbmc_printf2(sizeof_buffers, sizeof(buffers));
+  _cbmc_printf2(sizeof_buffers_0, sizeof(buffers[0]));
+  _cbmc_printf2(sizeof_buffer, sizeof(buffers[0]->buffer));
+
+  buffers[0]->buffer[0];
+  buffers[0]->buffer[BUFFER_SIZE - 1];
+  buffers[0]->buffer[BUFFER_SIZE]; // should be out-of-bounds
+}

regression/cbmc/memory_allocation2/test.desc

@@ -0,0 +1,11 @@
+CORE broken-smt-backend
+main.c
+--bounds-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$
+^\[main\.array_bounds\.[67]\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$
+^\*\* 2 of 7 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -169,7 +169,7 @@ class goto_checkt
 void goto_checkt::collect_allocations(
   const goto_functionst &goto_functions)
 {
-  if(!enable_pointer_check)
+  if(!enable_pointer_check && !enable_bounds_check)
     return;
 
   forall_goto_functions(itf, goto_functions)
@@ -1296,10 +1296,29 @@ void goto_checkt::bounds_check(
 
     binary_relation_exprt inequality(effective_offset, ID_lt, size_casted);
 
+    exprt::operandst alloc_disjuncts;
+    for(const auto &a : allocations)
+    {
+      typecast_exprt int_ptr{pointer, a.first.type()};
+
+      binary_relation_exprt lower_bound_check{a.first, ID_le, int_ptr};
+
+      plus_exprt upper_bound{
+        int_ptr,
+        typecast_exprt::conditional_cast(ode.offset(), int_ptr.type())};
+
+      binary_relation_exprt upper_bound_check{
+        std::move(upper_bound), ID_lt, plus_exprt{a.first, a.second}};
+
+      alloc_disjuncts.push_back(
+        and_exprt{std::move(lower_bound_check), std::move(upper_bound_check)});
+    }
+
+    exprt in_bounds_of_some_explicit_allocation = disjunction(alloc_disjuncts);
+
     or_exprt precond(
-      and_exprt(
-        dynamic_object(pointer),
-        not_exprt(malloc_object(pointer, ns))),
+      std::move(in_bounds_of_some_explicit_allocation),
+      and_exprt(dynamic_object(pointer), not_exprt(malloc_object(pointer, ns))),
       inequality);
 
     add_guarded_claim(