Merge pull request #5512 from feliperodri/update-posix_memalign

Updates posix_memalign to consider malloc may fail

Author: NlightNFotis

regression/cbmc-library/posix_memalign-01/test.desc

@@ -1,8 +1,8 @@
 CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --malloc-may-fail --malloc-fail-null
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$
 --
-^\*\*\*\* WARNING: no body for function posix_memalign
+^warning: ignoring

regression/cbmc-library/posix_memalign-02/main.c

@@ -0,0 +1,13 @@
+#include <stdlib.h>
+#include <string.h>
+
+int main()
+{
+  size_t size = 4;
+  size_t page_size = 4096;
+  void *src = "testing";
+  void *dest;
+  posix_memalign(&dest, page_size, size);
+  memcpy(dest, src, size);
+  return 0;
+}

regression/cbmc-library/posix_memalign-02/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check --bounds-check --malloc-may-fail --malloc-fail-null
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main.precondition_instance.1\] .* memcpy src/dst overlap: FAILURE
+\[main.precondition_instance.3\] .* memcpy destination region writeable: FAILURE
+\*\* 2 of 14 failed
+--
+^warning: ignoring

src/ansi-c/library/stdlib.c

@@ -527,20 +527,13 @@ __CPROVER_HIDE:;
   // As _mid_memalign simplifies for alignment <= MALLOC_ALIGNMENT
   // to a malloc call, it should be sound, if we do it too.
 
-  // The original posix_memalign check on the pointer is:
-
-  // void *tmp = malloc(size);
-  // if(tmp != NULL){
-  //   *ptr = tmp;
-  //   return 0;
-  // }
-  // return ENOMEM;
-
-  // As _CPROVER_allocate used in malloc never returns null,
-  // this check is not applicable and can be simplified:
-
-  *ptr = malloc(size);
-  return 0;
+  void *tmp = malloc(size);
+  if(tmp != (void *)0)
+  {
+    *ptr = tmp;
+    return 0;
+  }
+  return ENOMEM;
 }
 
 /* FUNCTION: random */