Merge pull request #5518 from hannes-steffenhagen-diffblue/fix/realloc-double-free

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

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;
 }