From 00b26a8fdeb19295f4e79f8afd2634eb479c0d5d Mon Sep 17 00:00:00 2001
From: Malte Mues <mail.mues@gmail.com>
Date: Mon, 30 Jul 2018 15:07:02 -0400
Subject: [PATCH] Adds a test for posix_memalign in stdlib.c

This commit tests the changes introduced in
15aa61f4acb865addf287f340dc0e3d1a3b0dbe6
---
 regression/cbmc/posix_memalign/main.c    | 16 ++++++++++++++++
 regression/cbmc/posix_memalign/test.desc |  8 ++++++++
 2 files changed, 24 insertions(+)
 create mode 100644 regression/cbmc/posix_memalign/main.c
 create mode 100644 regression/cbmc/posix_memalign/test.desc

diff --git a/regression/cbmc/posix_memalign/main.c b/regression/cbmc/posix_memalign/main.c
new file mode 100644
index 00000000000..1d0a76e901c
--- /dev/null
+++ b/regression/cbmc/posix_memalign/main.c
@@ -0,0 +1,16 @@
+#include <stdlib.h>
+#include <string.h>
+
+int main()
+{
+  size_t size = 4;
+  size_t page_size = 4096;
+  void *src = "testing";
+  void *dest;
+  if(posix_memalign(&dest, page_size, size))
+  {
+    return -1;
+  }
+  memcpy(dest, src, size);
+  return 0;
+}
diff --git a/regression/cbmc/posix_memalign/test.desc b/regression/cbmc/posix_memalign/test.desc
new file mode 100644
index 00000000000..3e2ef98ab4b
--- /dev/null
+++ b/regression/cbmc/posix_memalign/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^\*\*\*\* WARNING: no body for function posix_memalign