[RTL] Test case for aligned allocation

src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c

@@ -249,6 +249,7 @@ static void* bittree_store_block(void* ptr, size_t size) {
   tmp->is_readonly = false;
   tmp->freeable = false;
   bt_insert(tmp);
+  printf("Store block: %a %d\n", ptr, size);
   return tmp;
 }
 
@@ -259,6 +260,7 @@ static void bittree_delete_block(void* ptr) {
   DASSERT(tmp != NULL);
   bt_clean_block_init(tmp);
   bt_remove(tmp);
+  printf("Delete block: %a %d\n", ptr, tmp->size);
   native_free(tmp);
 }
 /* }}} */
@@ -320,7 +322,7 @@ static int bittree_posix_memalign(void **memptr, size_t alignment, size_t size)
    *  - size and alignment are greater than zero
    *  - alignment is a power of 2 and a multiple of sizeof(void*) */
   if (!size || !alignment || !powof2(alignment) || alignment%sizeof(void*))
-    return NULL;
+    return -1;
 
   /* Make sure that the first argument to posix memalign is indeed allocated */
   vassert(valid(memptr, sizeof(void*)),
@@ -408,6 +410,7 @@ static void bittree_free(void* ptr) {
     return;
   tmp = bt_lookup(ptr);
   DASSERT(tmp != NULL);
+  printf("Free block: %a %d\n", ptr, tmp->size);
   native_free(ptr);
   bt_clean_block_init(tmp);
   __e_acsl_heap_size -= tmp->size;
@@ -467,6 +470,8 @@ strong_alias(bittree_malloc,	malloc)
 strong_alias(bittree_calloc, calloc)
 strong_alias(bittree_realloc, realloc)
 strong_alias(bittree_free, free)
+strong_alias(bittree_posix_memalign, posix_memalign)
+strong_alias(bittree_aligned_alloc, aligned_alloc)
 strong_alias(bittree_delete_block, __e_acsl_delete_block)
 strong_alias(bittree_store_block, __e_acsl_store_block)
 strong_alias(offset, __e_acsl_offset)

src/plugins/e-acsl/tests/e-acsl-runtime/memalign.c

+/* run.config
+   COMMENT: Check aligned heap memory allocation
+*/
+
+#include <stdlib.h>
+
+int posix_memalign(void **memptr, size_t alignment, size_t size);
+void *aligned_alloc(size_t alignment, size_t size);
+
+int main(int argc, const char **argv) {
+  char **memptr = malloc(sizeof(void*));
+  int res2 = posix_memalign((void**)memptr, 256, 15);
+
+  char *p = *memptr;
+  /*@assert \valid(p); */
+  /*@assert \block_length(p) == 15; */
+  /*@assert \freeable(p); */
+  free(p);
+  /*@assert ! \valid(p); */
+
+  char *a;
+  a = aligned_alloc(256, 12);
+  /*@assert a == \null; */
+
+  a = aligned_alloc(255, 512);
+  /*@assert a == \null; */
+
+  a = aligned_alloc(0, 512);
+  /*@assert a == \null; */
+
+  a = aligned_alloc(256, 512);
+  /*@assert a != \null; */
+  /*@assert \valid(a); */
+  /*@assert \block_length(a) == 512; */
+  /*@assert \freeable(a); */
+
+  free(a);
+  /*@assert ! \valid(a); */
+
+  return 0;
+}

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memalign.c

+/* Generated by Frama-C */
+int main(int argc, char const **argv)
+{
+  int __retres;
+  char **memptr;
+  int res2;
+  char *p;
+  char *a;
+  __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
+  __e_acsl_store_block((void *)(& a),8UL);
+  __e_acsl_store_block((void *)(& p),8UL);
+  __e_acsl_store_block((void *)(& memptr),8UL);
+  __e_acsl_full_init((void *)(& memptr));
+  memptr = (char **)malloc(sizeof(void *));
+  res2 = posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15);
+  __e_acsl_full_init((void *)(& p));
+  /*@ assert Value: mem_access: \valid_read(memptr); */
+  p = *memptr;
+  /*@ assert \valid(p); */
+  {
+    int __gen_e_acsl_initialized;
+    int __gen_e_acsl_and;
+    __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+                                                    sizeof(char *));
+    if (__gen_e_acsl_initialized) {
+      int __gen_e_acsl_valid;
+      __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(char));
+      __gen_e_acsl_and = __gen_e_acsl_valid;
+    }
+    else __gen_e_acsl_and = 0;
+    __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+                    (char *)"\\valid(p)",15);
+  }
+  /*@ assert \block_length(p) ≡ 15; */
+  {
+    unsigned long __gen_e_acsl_block_length;
+    __gen_e_acsl_block_length = __e_acsl_block_length((void *)p);
+    __e_acsl_assert(__gen_e_acsl_block_length == 15,(char *)"Assertion",
+                    (char *)"main",(char *)"\\block_length(p) == 15",16);
+  }
+  /*@ assert \freeable(p); */
+  {
+    int __gen_e_acsl_freeable;
+    __gen_e_acsl_freeable = __e_acsl_freeable((void *)p);
+    __e_acsl_assert(__gen_e_acsl_freeable,(char *)"Assertion",(char *)"main",
+                    (char *)"\\freeable(p)",17);
+  }
+  free((void *)p);
+  /*@ assert ¬\valid(p); */
+  {
+    int __gen_e_acsl_initialized_2;
+    int __gen_e_acsl_and_2;
+    __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& p),
+                                                      sizeof(char *));
+    if (__gen_e_acsl_initialized_2) {
+      int __gen_e_acsl_valid_2;
+      __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(char));
+      __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
+    }
+    else __gen_e_acsl_and_2 = 0;
+    __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",(char *)"main",
+                    (char *)"!\\valid(p)",19);
+  }
+  __e_acsl_full_init((void *)(& a));
+  a = (char *)aligned_alloc((unsigned long)256,(unsigned long)12);
+  /*@ assert a ≡ \null; */
+  __e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
+                  (char *)"a == \\null",23);
+  __e_acsl_full_init((void *)(& a));
+  a = (char *)aligned_alloc((unsigned long)255,(unsigned long)512);
+  /*@ assert a ≡ \null; */
+  __e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
+                  (char *)"a == \\null",26);
+  __e_acsl_full_init((void *)(& a));
+  a = (char *)aligned_alloc((unsigned long)0,(unsigned long)512);
+  /*@ assert a ≡ \null; */
+  __e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
+                  (char *)"a == \\null",29);
+  __e_acsl_full_init((void *)(& a));
+  a = (char *)aligned_alloc((unsigned long)256,(unsigned long)512);
+  /*@ assert a ≢ \null; */
+  __e_acsl_assert(a != (void *)0,(char *)"Assertion",(char *)"main",
+                  (char *)"a != \\null",32);
+  /*@ assert \valid(a); */
+  {
+    int __gen_e_acsl_initialized_3;
+    int __gen_e_acsl_and_3;
+    __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& a),
+                                                      sizeof(char *));
+    if (__gen_e_acsl_initialized_3) {
+      int __gen_e_acsl_valid_3;
+      __gen_e_acsl_valid_3 = __e_acsl_valid((void *)a,sizeof(char));
+      __gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
+    }
+    else __gen_e_acsl_and_3 = 0;
+    __e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion",(char *)"main",
+                    (char *)"\\valid(a)",33);
+  }
+  /*@ assert \block_length(a) ≡ 512; */
+  {
+    unsigned long __gen_e_acsl_block_length_2;
+    __gen_e_acsl_block_length_2 = __e_acsl_block_length((void *)a);
+    __e_acsl_assert(__gen_e_acsl_block_length_2 == 512,(char *)"Assertion",
+                    (char *)"main",(char *)"\\block_length(a) == 512",34);
+  }
+  /*@ assert \freeable(a); */
+  {
+    int __gen_e_acsl_freeable_2;
+    __gen_e_acsl_freeable_2 = __e_acsl_freeable((void *)a);
+    __e_acsl_assert(__gen_e_acsl_freeable_2,(char *)"Assertion",
+                    (char *)"main",(char *)"\\freeable(a)",35);
+  }
+  free((void *)a);
+  /*@ assert ¬\valid(a); */
+  {
+    int __gen_e_acsl_initialized_4;
+    int __gen_e_acsl_and_4;
+    __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& a),
+                                                      sizeof(char *));
+    if (__gen_e_acsl_initialized_4) {
+      int __gen_e_acsl_valid_4;
+      __gen_e_acsl_valid_4 = __e_acsl_valid((void *)a,sizeof(char));
+      __gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
+    }
+    else __gen_e_acsl_and_4 = 0;
+    __e_acsl_assert(! __gen_e_acsl_and_4,(char *)"Assertion",(char *)"main",
+                    (char *)"!\\valid(a)",38);
+  }
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& a));
+  __e_acsl_delete_block((void *)(& p));
+  __e_acsl_delete_block((void *)(& memptr));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memalign.res.oracle

+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+tests/e-acsl-runtime/memalign.c:12:[kernel] warning: Neither code nor specification for function posix_memalign, generating default assigns from the prototype
+tests/e-acsl-runtime/memalign.c:14:[value] warning: out of bounds read. assert \valid_read(memptr);
+tests/e-acsl-runtime/memalign.c:15:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/memalign.c:16:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:17:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
+tests/e-acsl-runtime/memalign.c:19:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:22:[kernel] warning: Neither code nor specification for function aligned_alloc, generating default assigns from the prototype
+tests/e-acsl-runtime/memalign.c:23:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:26:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:29:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:32:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:33:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/memalign.c:34:[value] warning: assertion got status invalid (stopping propagation).