Improves regression tests for posix_memalign

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

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