Contracts test: ensure return value access is in bounds

We ended up with an assumption that performed an out-of-bounds access as
there was no link between `size` and the return value in the contract.

Author: tautschnig

regression/contracts/assigns-replace-malloc-zero/main.c

@@ -8,7 +8,8 @@ __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
 __CPROVER_requires(a == NULL || __CPROVER_rw_ok(a, size))
 __CPROVER_assigns(__CPROVER_object_whole(a))
 __CPROVER_ensures(
-    a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
+    a && __CPROVER_return_value >= 0 ==>
+         (__CPROVER_return_value < size && a[__CPROVER_return_value] == 0))
 // clang-format on
 {
   if(!a)

regression/contracts/assigns-replace-malloc-zero/test.desc

@@ -4,7 +4,7 @@ main.c
 ^\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
-\[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$
+\[main\.assertion\.1\] line 36 expecting SUCCESS: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that objects of size zero or of __CPROVER_max_malloc_size