diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index 199cbde0cec2f98c7ab41aa6dbb86ee0fe01189f..e9fec5e0c3b60c1e21e80d0a79017a10d3ac61fd 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/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)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/memalign.c b/src/plugins/e-acsl/tests/e-acsl-runtime/memalign.c
new file mode 100644
index 0000000000000000000000000000000000000000..f88e16873420998d41e04aa21655e3ae9524e8c3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/memalign.c
@@ -0,0 +1,41 @@
+/* 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;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memalign.c
new file mode 100644
index 0000000000000000000000000000000000000000..e07c52b758badeeadade797bac128254980b00dc
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memalign.c
@@ -0,0 +1,137 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memalign.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memalign.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memalign.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..48ed44b405da8727e629464d8dc8762c5640be83
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memalign.res.oracle
@@ -0,0 +1,18 @@
+[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).