Fix double-free bug in stdlib models with --malloc-fail-null

If realloc results in a larger memory block the old one needs to be
freed... but this should only happen if the allocation of the new block
succeeds. The old model didn't properly check for that, this is now
fixed.

Author: hannes-steffenhagen-diffblue

regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.c

@@ -0,0 +1,17 @@
+#include <stdlib.h>
+
+int main(void)
+{
+  void *ptr = malloc(sizeof(char));
+  if(ptr == NULL)
+    return 0;
+
+  void *ptr1 = realloc(ptr, 2 * sizeof(char));
+  if(ptr1 == NULL)
+  {
+    free(ptr);
+    return 0;
+  }
+
+  free(ptr1);
+}

regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--malloc-may-fail --malloc-fail-null
+^\[main.precondition_instance.\d+] line \d+ double free: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This is a test checking for a regression where the --malloc-may-fail flag
+introduced a double-free bug in the stdlib models with realloc.

src/ansi-c/library/stdlib.c

@@ -477,8 +477,10 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
   void *res;
   res=malloc(malloc_size);
   if(res != (void *)0)
+  {
     __CPROVER_array_copy(res, ptr);
-  free(ptr);
+    free(ptr);
+  }
 
   return res;
 }