Change goto_checkt::address_check() dynamic memory bounds checking

This changes the dynamic memory bounds checking predicate in address_check().
It now uses OBJECT_SIZE() instead of the variables __CPROVER_malloc_size and
__CPROVER_malloc_object that are set in the malloc() model. This also means that
the predicates __CPROVER_r_ok()/__CPROVER_w_ok() will be more precise. In the
previous approach, the following assertion could not be proven for example:

void main() { char *c = malloc(1); assert(!__CPROVER_r_ok(c, 2)); }

Author: danpoe

regression/cbmc/r_w_ok5/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char c[2];
+  assert(__CPROVER_r_ok(c, 3));
+  assert(!__CPROVER_r_ok(c, 3));
+
+  char *p = malloc(2);
+  assert(__CPROVER_r_ok(p, 3));
+  assert(!__CPROVER_r_ok(p, 3));
+}

regression/cbmc/r_w_ok5/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+\[main.assertion.1\] .*: FAILURE
+\[main.assertion.2\] .*: SUCCESS
+\[main.assertion.3\] .*: FAILURE
+\[main.assertion.4\] .*: SUCCESS
+\*\* 2 of 4 failed
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/r_w_ok6/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p;
+  int choice;
+
+  if (choice) {
+    p = malloc(2);
+  }
+  else
+  {
+    p = malloc(3);
+  }
+
+  assert(__CPROVER_r_ok(p, 2));
+  assert(!__CPROVER_r_ok(p, 2));
+
+  assert(__CPROVER_r_ok(p, 3));
+  assert(!__CPROVER_r_ok(p, 3));
+
+  assert(__CPROVER_r_ok(p, 4));
+  assert(!__CPROVER_r_ok(p, 4));
+}

regression/cbmc/r_w_ok6/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+
+\[main.assertion.1\] .*: SUCCESS
+\[main.assertion.2\] .*: FAILURE
+\[main.assertion.3\] .*: FAILURE
+\[main.assertion.4\] .*: FAILURE
+\[main.assertion.5\] .*: FAILURE
+\[main.assertion.6\] .*: SUCCESS
+\*\* 4 of 6 failed
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/r_w_ok7/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  size_t x;
+  size_t y;
+  uint8_t *a;
+
+  __CPROVER_assume(x > 0);
+  __CPROVER_assume(y > x);
+
+  a = malloc(sizeof(*(a)) * (x));
+
+  assert(!__CPROVER_w_ok(a, y));
+}

regression/cbmc/r_w_ok7/test.desc

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

regression/cbmc/r_w_ok8/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *x = malloc(2);
+  int *y = malloc(2);
+  assert(__CPROVER_r_ok(x, 3) == __CPROVER_r_ok(y, 3));
+}

regression/cbmc/r_w_ok8/test.desc

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

src/analyses/goto_check.cpp

@@ -1249,15 +1249,15 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
 
     if(flags.is_unknown() || flags.is_dynamic_heap())
     {
-      const or_exprt dynamic_bounds_violation(
-        dynamic_object_lower_bound(address, nil_exprt()),
-        dynamic_object_upper_bound(address, ns, size));
+      const or_exprt object_bounds_violation(
+        object_lower_bound(address, nil_exprt()),
+        object_upper_bound(address, size));
 
       conditions.push_back(conditiont(
         or_exprt(
           in_bounds_of_some_explicit_allocation,
           implies_exprt(
-            malloc_object(address, ns), not_exprt(dynamic_bounds_violation))),
+            dynamic_object(address), not_exprt(object_bounds_violation))),
         "pointer outside dynamic object bounds"));
     }