From 431e8f57dc8f8ca229017c7ea4086540d029ce19 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Thu, 7 Jan 2016 10:54:52 +0100
Subject: [PATCH] Added a testcase for checking whether the tracked heap size
(__memory_size) is computed correctly
---
.../e-acsl/tests/e-acsl-runtime/memsize.c | 73 +++
.../tests/e-acsl-runtime/oracle/gen_memsize.c | 325 ++++++++++++
.../e-acsl-runtime/oracle/gen_memsize2.c | 490 ++++++++++++++++++
.../oracle/memsize.0.err.oracle | 0
.../oracle/memsize.0.res.oracle | 64 +++
.../oracle/memsize.1.err.oracle | 0
.../oracle/memsize.1.res.oracle | 61 +++
7 files changed, 1013 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize2.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c b/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
new file mode 100644
index 00000000000..1d630e2aaaf
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/memsize.c
@@ -0,0 +1,73 @@
+/* run.config
+ COMMENT: Checking heap memory size
+ EXECNOW: LOG gen_memsize.c BIN gen_memsize.out @frama-c@ -machdep=gcc_x86_$(getconf LONG_BIT) -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/memsize.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_memsize.c > /dev/null && ./gcc_runtime.sh memsize
+ EXECNOW: LOG gen_memsize2.c BIN gen_memsize2.out @frama-c@ -machdep=gcc_x86_$(getconf LONG_BIT) -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/memsize.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_memsize2.c > /dev/null && ./gcc_runtime.sh memsize2
+*/
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <stdint.h>
+
+# ifndef UINTPTR_MAX
+# if __WORDSIZE == 64
+# define UINTPTR_MAX (18446744073709551615UL)
+# else
+# define UINTPTR_MAX (4294967295U)
+# endif
+# endif
+
+extern size_t __memory_size;
+
+int main(int argc, char **argv) {
+ // Allocation increases
+ char *a = malloc(7);
+ /*@assert (__memory_size == 7); */
+ char *b = malloc(14);
+ /*@assert (__memory_size == 21); */
+
+ // Allocation decreases
+ free(a);
+ /*@assert (__memory_size == 14); */
+
+ // Make sure that free with NULL behaves and does not affect allocation
+ a = NULL;
+ free(a);
+ /*@assert (__memory_size == 14); */
+
+ // Realloc decreases allocation
+ b = realloc(b, 9);
+ /*@assert (__memory_size == 9); */
+
+ // Realloc increases allocation
+ b = realloc(b, 18);
+ /*@assert (__memory_size == 18); */
+
+ // Realloc with 0 is equivalent to free
+ b = realloc(b, 0);
+ b = NULL;
+ /*@assert (__memory_size == 0); */
+
+ // realloc with 0 is equivalent to malloc
+ b = realloc(b, 8);
+ /*@assert (__memory_size == 8); */
+
+ // Abandon b and behave like malloc again
+ b = realloc(NULL, 8);
+ /*@assert (__memory_size == 16); */
+
+ // Make realloc fail by supplying a huge number
+ b = realloc(NULL, UINTPTR_MAX);
+ /*@assert (__memory_size == 16); */
+ /*@assert (b == NULL); */
+
+ // Same as test for calloc ...
+ b = calloc(UINTPTR_MAX,UINTPTR_MAX);
+ /*@assert (__memory_size == 16); */
+ /*@assert (b == NULL); */
+
+ // ... and for malloc
+ b = malloc(UINTPTR_MAX);
+ /*@assert (__memory_size == 16); */
+ /*@assert (b == NULL); */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
new file mode 100644
index 00000000000..d3d869e4813
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
@@ -0,0 +1,325 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned long size_t;
+typedef unsigned int ino_t;
+typedef unsigned int gid_t;
+typedef unsigned int uid_t;
+typedef long time_t;
+typedef unsigned int blkcnt_t;
+typedef unsigned int blksize_t;
+typedef unsigned int dev_t;
+typedef unsigned int mode_t;
+typedef unsigned int nlink_t;
+typedef long off_t;
+struct stat {
+ dev_t st_dev ;
+ ino_t st_ino ;
+ mode_t st_mode ;
+ nlink_t st_nlink ;
+ uid_t st_uid ;
+ gid_t st_gid ;
+ dev_t st_rdev ;
+ off_t st_size ;
+ time_t st_atime ;
+ time_t st_mtime ;
+ time_t st_ctime ;
+ blksize_t st_blksize ;
+ blkcnt_t st_blocks ;
+};
+struct __fc_pos_t {
+ unsigned long __fc_stdio_position ;
+};
+typedef struct __fc_pos_t fpos_t;
+struct __fc_FILE {
+ unsigned int __fc_stdio_id ;
+ fpos_t __fc_position ;
+ char __fc_error ;
+ char __fc_eof ;
+ int __fc_flags ;
+ struct stat *__fc_inode ;
+ unsigned char *__fc_real_data ;
+ int __fc_real_data_max_size ;
+};
+typedef struct __fc_FILE FILE;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+void *__malloc(size_t size);
+
+void __free(void *p);
+
+void *__realloc(void *ptr, size_t size);
+
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void *__e_acsl_malloc(size_t size)
+{
+ void *__retres;
+ __store_block((void *)(& __retres),8UL);
+ __retres = __malloc(size);
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
+
+ behavior deallocation:
+ assumes p ≢ \null;
+ requires freeable: \freeable(p);
+ ensures \allocable(\old(p));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+
+ behavior no_deallocation:
+ assumes p ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_deallocation, deallocation;
+ disjoint behaviors no_deallocation, deallocation;
+ */
+void __e_acsl_free(void *p)
+{
+ int __e_acsl_at;
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),8UL);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",178);
+ __store_block((void *)(& __e_acsl_at),4UL);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
+ __delete_block((void *)(& p));
+ return;
+}
+
+/*@ requires ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from __fc_heap_status;
+ assigns \result \from size, ptr, __fc_heap_status;
+ frees ptr;
+ allocates \result;
+
+ behavior alloc:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns \result;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior dealloc:
+ assumes ptr ≢ \null;
+ assumes is_allocable(size);
+ requires \freeable(ptr);
+ ensures \allocable(\old(ptr));
+ ensures \result ≡ \null ∨ \freeable(\result);
+ frees ptr;
+
+ behavior fail:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result;
+ assigns \result \from size, __fc_heap_status;
+ allocates \nothing;
+
+ complete behaviors fail, dealloc, alloc;
+ disjoint behaviors dealloc, fail;
+ disjoint behaviors alloc, fail;
+ */
+void *__e_acsl_realloc(void *ptr, size_t size)
+{
+ void *__retres;
+ __store_block((void *)(& __retres),8UL);
+ {
+ int __e_acsl_or;
+ __store_block((void *)(& ptr),8UL);
+ if (ptr == (void *)0) __e_acsl_or = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(ptr);
+ __e_acsl_or = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_or,(char *)"Precondition",(char *)"realloc",
+ (char *)"ptr == \\null || \\freeable(ptr)",201);
+ __retres = __realloc(ptr,size);
+ }
+ __delete_block((void *)(& ptr));
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+
+*/
+void *__calloc(size_t nmemb, size_t size);
+
+FILE __fc_fopen[512];
+FILE * const __p_fc_fopen = __fc_fopen;
+int main(int argc, char **argv)
+{
+ int __retres;
+ char *a;
+ char *b;
+ __store_block((void *)(& b),8UL);
+ __store_block((void *)(& a),8UL);
+ __full_init((void *)(& a));
+ a = (char *)__e_acsl_malloc((unsigned long)7);
+ /*@ assert __memory_size ≡ 7; */
+ e_acsl_assert(__memory_size == (unsigned long)7,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 7",24);
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_malloc((unsigned long)14);
+ /*@ assert __memory_size ≡ 21; */
+ e_acsl_assert(__memory_size == (unsigned long)21,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 21",26);
+ __e_acsl_free((void *)a);
+ /*@ assert __memory_size ≡ 14; */
+ e_acsl_assert(__memory_size == (unsigned long)14,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 14",30);
+ __full_init((void *)(& a));
+ a = (char *)0;
+ __e_acsl_free((void *)a);
+ /*@ assert __memory_size ≡ 14; */
+ e_acsl_assert(__memory_size == (unsigned long)14,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 14",35);
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)b,(unsigned long)9);
+ /*@ assert __memory_size ≡ 9; */
+ e_acsl_assert(__memory_size == (unsigned long)9,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 9",39);
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)b,(unsigned long)18);
+ /*@ assert __memory_size ≡ 18; */
+ e_acsl_assert(__memory_size == (unsigned long)18,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 18",43);
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)b,(unsigned long)0);
+ __full_init((void *)(& b));
+ b = (char *)0;
+ /*@ assert __memory_size ≡ 0; */
+ e_acsl_assert(__memory_size == (unsigned long)0,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 0",48);
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)b,(unsigned long)8);
+ /*@ assert __memory_size ≡ 8; */
+ e_acsl_assert(__memory_size == (unsigned long)8,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 8",52);
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)0,(unsigned long)8);
+ /*@ assert __memory_size ≡ 16; */
+ e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 16",56);
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)0,18446744073709551615UL);
+ /*@ assert __memory_size ≡ 16; */
+ e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 16",60);
+ /*@ assert b ≡ (char *)((void *)0); */
+ e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
+ (char *)"b == (char *)((void *)0)",61);
+ __full_init((void *)(& b));
+ b = (char *)__calloc(18446744073709551615UL,18446744073709551615UL);
+ /*@ assert __memory_size ≡ 16; */
+ e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 16",65);
+ /*@ assert b ≡ (char *)((void *)0); */
+ e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
+ (char *)"b == (char *)((void *)0)",66);
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_malloc(18446744073709551615UL);
+ /*@ assert __memory_size ≡ 16; */
+ e_acsl_assert(__memory_size == (unsigned long)16,(char *)"Assertion",
+ (char *)"main",(char *)"__memory_size == 16",70);
+ /*@ assert b ≡ (char *)((void *)0); */
+ e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
+ (char *)"b == (char *)((void *)0)",71);
+ __retres = 0;
+ __delete_block((void *)(& b));
+ __delete_block((void *)(& a));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize2.c
new file mode 100644
index 00000000000..1b8a9bb8400
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize2.c
@@ -0,0 +1,490 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned long size_t;
+typedef unsigned int ino_t;
+typedef unsigned int gid_t;
+typedef unsigned int uid_t;
+typedef long time_t;
+typedef unsigned int blkcnt_t;
+typedef unsigned int blksize_t;
+typedef unsigned int dev_t;
+typedef unsigned int mode_t;
+typedef unsigned int nlink_t;
+typedef long off_t;
+struct stat {
+ dev_t st_dev ;
+ ino_t st_ino ;
+ mode_t st_mode ;
+ nlink_t st_nlink ;
+ uid_t st_uid ;
+ gid_t st_gid ;
+ dev_t st_rdev ;
+ off_t st_size ;
+ time_t st_atime ;
+ time_t st_mtime ;
+ time_t st_ctime ;
+ blksize_t st_blksize ;
+ blkcnt_t st_blocks ;
+};
+struct __fc_pos_t {
+ unsigned long __fc_stdio_position ;
+};
+typedef struct __fc_pos_t fpos_t;
+struct __fc_FILE {
+ unsigned int __fc_stdio_id ;
+ fpos_t __fc_position ;
+ char __fc_error ;
+ char __fc_eof ;
+ int __fc_flags ;
+ struct stat *__fc_inode ;
+ unsigned char *__fc_real_data ;
+ int __fc_real_data_max_size ;
+};
+typedef struct __fc_FILE FILE;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+void *__malloc(size_t size);
+
+void __free(void *p);
+
+void *__realloc(void *ptr, size_t size);
+
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ ensures \initialized(\old(z));
+ assigns *z;
+ assigns *z \from n;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z,
+ unsigned long n);
+
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ ensures \initialized(\old(z));
+ assigns *z;
+ assigns *z \from n;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
+ long n);
+
+/*@ requires \valid(x);
+ assigns *x;
+ assigns *x \from *x; */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
+ assigns \result;
+ assigns \result \from *z1, *z2;
+ */
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void *__e_acsl_malloc(size_t size)
+{
+ void *__retres;
+ __store_block((void *)(& __retres),8UL);
+ __retres = __malloc(size);
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
+
+ behavior deallocation:
+ assumes p ≢ \null;
+ requires freeable: \freeable(p);
+ ensures \allocable(\old(p));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+
+ behavior no_deallocation:
+ assumes p ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_deallocation, deallocation;
+ disjoint behaviors no_deallocation, deallocation;
+ */
+void __e_acsl_free(void *p)
+{
+ int __e_acsl_at;
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),8UL);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",178);
+ __store_block((void *)(& __e_acsl_at),4UL);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
+ __delete_block((void *)(& p));
+ return;
+}
+
+/*@ requires ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from __fc_heap_status;
+ assigns \result \from size, ptr, __fc_heap_status;
+ frees ptr;
+ allocates \result;
+
+ behavior alloc:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns \result;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior dealloc:
+ assumes ptr ≢ \null;
+ assumes is_allocable(size);
+ requires \freeable(ptr);
+ ensures \allocable(\old(ptr));
+ ensures \result ≡ \null ∨ \freeable(\result);
+ frees ptr;
+
+ behavior fail:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result;
+ assigns \result \from size, __fc_heap_status;
+ allocates \nothing;
+
+ complete behaviors fail, dealloc, alloc;
+ disjoint behaviors dealloc, fail;
+ disjoint behaviors alloc, fail;
+ */
+void *__e_acsl_realloc(void *ptr, size_t size)
+{
+ void *__retres;
+ __store_block((void *)(& __retres),8UL);
+ {
+ int __e_acsl_or;
+ __store_block((void *)(& ptr),8UL);
+ if (ptr == (void *)0) __e_acsl_or = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(ptr);
+ __e_acsl_or = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_or,(char *)"Precondition",(char *)"realloc",
+ (char *)"ptr == \\null || \\freeable(ptr)",201);
+ __retres = __realloc(ptr,size);
+ }
+ __delete_block((void *)(& ptr));
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+
+*/
+void *__calloc(size_t nmemb, size_t size);
+
+FILE __fc_fopen[512];
+FILE * const __p_fc_fopen = __fc_fopen;
+int main(int argc, char **argv)
+{
+ int __retres;
+ char *a;
+ char *b;
+ __store_block((void *)(& b),8UL);
+ __store_block((void *)(& a),8UL);
+ __full_init((void *)(& a));
+ a = (char *)__e_acsl_malloc((unsigned long)7);
+ /*@ assert __memory_size ≡ 7; */
+ {
+ mpz_t __e_acsl___memory_size;
+ mpz_t __e_acsl;
+ int __e_acsl_eq;
+ __gmpz_init_set_ui(__e_acsl___memory_size,__memory_size);
+ __gmpz_init_set_si(__e_acsl,(long)7);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size),
+ (__mpz_struct const *)(__e_acsl));
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 7",24);
+ __gmpz_clear(__e_acsl___memory_size);
+ __gmpz_clear(__e_acsl);
+ }
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_malloc((unsigned long)14);
+ /*@ assert __memory_size ≡ 21; */
+ {
+ mpz_t __e_acsl___memory_size_2;
+ mpz_t __e_acsl_2;
+ int __e_acsl_eq_2;
+ __gmpz_init_set_ui(__e_acsl___memory_size_2,__memory_size);
+ __gmpz_init_set_si(__e_acsl_2,(long)21);
+ __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size_2),
+ (__mpz_struct const *)(__e_acsl_2));
+ e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 21",26);
+ __gmpz_clear(__e_acsl___memory_size_2);
+ __gmpz_clear(__e_acsl_2);
+ }
+ __e_acsl_free((void *)a);
+ /*@ assert __memory_size ≡ 14; */
+ {
+ mpz_t __e_acsl___memory_size_3;
+ mpz_t __e_acsl_3;
+ int __e_acsl_eq_3;
+ __gmpz_init_set_ui(__e_acsl___memory_size_3,__memory_size);
+ __gmpz_init_set_si(__e_acsl_3,(long)14);
+ __e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size_3),
+ (__mpz_struct const *)(__e_acsl_3));
+ e_acsl_assert(__e_acsl_eq_3 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 14",30);
+ __gmpz_clear(__e_acsl___memory_size_3);
+ __gmpz_clear(__e_acsl_3);
+ }
+ __full_init((void *)(& a));
+ a = (char *)0;
+ __e_acsl_free((void *)a);
+ /*@ assert __memory_size ≡ 14; */
+ {
+ mpz_t __e_acsl___memory_size_4;
+ mpz_t __e_acsl_4;
+ int __e_acsl_eq_4;
+ __gmpz_init_set_ui(__e_acsl___memory_size_4,__memory_size);
+ __gmpz_init_set_si(__e_acsl_4,(long)14);
+ __e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size_4),
+ (__mpz_struct const *)(__e_acsl_4));
+ e_acsl_assert(__e_acsl_eq_4 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 14",35);
+ __gmpz_clear(__e_acsl___memory_size_4);
+ __gmpz_clear(__e_acsl_4);
+ }
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)b,(unsigned long)9);
+ /*@ assert __memory_size ≡ 9; */
+ {
+ mpz_t __e_acsl___memory_size_5;
+ mpz_t __e_acsl_5;
+ int __e_acsl_eq_5;
+ __gmpz_init_set_ui(__e_acsl___memory_size_5,__memory_size);
+ __gmpz_init_set_si(__e_acsl_5,(long)9);
+ __e_acsl_eq_5 = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size_5),
+ (__mpz_struct const *)(__e_acsl_5));
+ e_acsl_assert(__e_acsl_eq_5 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 9",39);
+ __gmpz_clear(__e_acsl___memory_size_5);
+ __gmpz_clear(__e_acsl_5);
+ }
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)b,(unsigned long)18);
+ /*@ assert __memory_size ≡ 18; */
+ {
+ mpz_t __e_acsl___memory_size_6;
+ mpz_t __e_acsl_6;
+ int __e_acsl_eq_6;
+ __gmpz_init_set_ui(__e_acsl___memory_size_6,__memory_size);
+ __gmpz_init_set_si(__e_acsl_6,(long)18);
+ __e_acsl_eq_6 = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size_6),
+ (__mpz_struct const *)(__e_acsl_6));
+ e_acsl_assert(__e_acsl_eq_6 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 18",43);
+ __gmpz_clear(__e_acsl___memory_size_6);
+ __gmpz_clear(__e_acsl_6);
+ }
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)b,(unsigned long)0);
+ __full_init((void *)(& b));
+ b = (char *)0;
+ /*@ assert __memory_size ≡ 0; */
+ {
+ mpz_t __e_acsl___memory_size_7;
+ mpz_t __e_acsl_7;
+ int __e_acsl_eq_7;
+ __gmpz_init_set_ui(__e_acsl___memory_size_7,__memory_size);
+ __gmpz_init_set_si(__e_acsl_7,(long)0);
+ __e_acsl_eq_7 = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size_7),
+ (__mpz_struct const *)(__e_acsl_7));
+ e_acsl_assert(__e_acsl_eq_7 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 0",48);
+ __gmpz_clear(__e_acsl___memory_size_7);
+ __gmpz_clear(__e_acsl_7);
+ }
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)b,(unsigned long)8);
+ /*@ assert __memory_size ≡ 8; */
+ {
+ mpz_t __e_acsl___memory_size_8;
+ mpz_t __e_acsl_8;
+ int __e_acsl_eq_8;
+ __gmpz_init_set_ui(__e_acsl___memory_size_8,__memory_size);
+ __gmpz_init_set_si(__e_acsl_8,(long)8);
+ __e_acsl_eq_8 = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size_8),
+ (__mpz_struct const *)(__e_acsl_8));
+ e_acsl_assert(__e_acsl_eq_8 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 8",52);
+ __gmpz_clear(__e_acsl___memory_size_8);
+ __gmpz_clear(__e_acsl_8);
+ }
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)0,(unsigned long)8);
+ /*@ assert __memory_size ≡ 16; */
+ {
+ mpz_t __e_acsl___memory_size_9;
+ mpz_t __e_acsl_9;
+ int __e_acsl_eq_9;
+ __gmpz_init_set_ui(__e_acsl___memory_size_9,__memory_size);
+ __gmpz_init_set_si(__e_acsl_9,(long)16);
+ __e_acsl_eq_9 = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size_9),
+ (__mpz_struct const *)(__e_acsl_9));
+ e_acsl_assert(__e_acsl_eq_9 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 16",56);
+ __gmpz_clear(__e_acsl___memory_size_9);
+ __gmpz_clear(__e_acsl_9);
+ }
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_realloc((void *)0,18446744073709551615UL);
+ /*@ assert __memory_size ≡ 16; */
+ {
+ mpz_t __e_acsl___memory_size_10;
+ mpz_t __e_acsl_10;
+ int __e_acsl_eq_10;
+ __gmpz_init_set_ui(__e_acsl___memory_size_10,__memory_size);
+ __gmpz_init_set_si(__e_acsl_10,(long)16);
+ __e_acsl_eq_10 = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size_10),
+ (__mpz_struct const *)(__e_acsl_10));
+ e_acsl_assert(__e_acsl_eq_10 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 16",60);
+ __gmpz_clear(__e_acsl___memory_size_10);
+ __gmpz_clear(__e_acsl_10);
+ }
+ /*@ assert b ≡ (char *)((void *)0); */
+ e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
+ (char *)"b == (char *)((void *)0)",61);
+ __full_init((void *)(& b));
+ b = (char *)__calloc(18446744073709551615UL,18446744073709551615UL);
+ /*@ assert __memory_size ≡ 16; */
+ {
+ mpz_t __e_acsl___memory_size_11;
+ mpz_t __e_acsl_11;
+ int __e_acsl_eq_11;
+ __gmpz_init_set_ui(__e_acsl___memory_size_11,__memory_size);
+ __gmpz_init_set_si(__e_acsl_11,(long)16);
+ __e_acsl_eq_11 = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size_11),
+ (__mpz_struct const *)(__e_acsl_11));
+ e_acsl_assert(__e_acsl_eq_11 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 16",65);
+ __gmpz_clear(__e_acsl___memory_size_11);
+ __gmpz_clear(__e_acsl_11);
+ }
+ /*@ assert b ≡ (char *)((void *)0); */
+ e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
+ (char *)"b == (char *)((void *)0)",66);
+ __full_init((void *)(& b));
+ b = (char *)__e_acsl_malloc(18446744073709551615UL);
+ /*@ assert __memory_size ≡ 16; */
+ {
+ mpz_t __e_acsl___memory_size_12;
+ mpz_t __e_acsl_12;
+ int __e_acsl_eq_12;
+ __gmpz_init_set_ui(__e_acsl___memory_size_12,__memory_size);
+ __gmpz_init_set_si(__e_acsl_12,(long)16);
+ __e_acsl_eq_12 = __gmpz_cmp((__mpz_struct const *)(__e_acsl___memory_size_12),
+ (__mpz_struct const *)(__e_acsl_12));
+ e_acsl_assert(__e_acsl_eq_12 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__memory_size == 16",70);
+ __gmpz_clear(__e_acsl___memory_size_12);
+ __gmpz_clear(__e_acsl_12);
+ }
+ /*@ assert b ≡ (char *)((void *)0); */
+ e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
+ (char *)"b == (char *)((void *)0)",71);
+ __retres = 0;
+ __delete_block((void *)(& b));
+ __delete_block((void *)(& a));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle
new file mode 100644
index 00000000000..4769e9abc32
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle
@@ -0,0 +1,64 @@
+[e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `realloc':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:200:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:200:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/memsize.c:21:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/memsize.c:21:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/memsize.c:21:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:215:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:215:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:208:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:222:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:146:[kernel] warning: Neither code nor specification for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+ __fc_fopen[0..511] ∈ {0}
+ __p_fc_fopen ∈ {{ &__fc_fopen[0] }}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __malloc
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/memsize.c:24:[value] Assertion got status unknown.
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+tests/e-acsl-runtime/memsize.c:26:[value] Assertion got status invalid (stopping propagation).
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle
new file mode 100644
index 00000000000..b5e711cfb61
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle
@@ -0,0 +1,61 @@
+[e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `realloc':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:200:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:200:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/memsize.c:21:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/memsize.c:21:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/memsize.c:21:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/memsize.c:21:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:214:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:214:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:146:[kernel] warning: Neither code nor specification for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+ __fc_fopen[0..511] ∈ {0}
+ __p_fc_fopen ∈ {{ &__fc_fopen[0] }}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __malloc
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/memsize.c:24:[value] Assertion got status unknown.
+[value] using specification for function __gmpz_init_set_ui
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
+[value] using specification for function __gmpz_init_set_si
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
+[value] using specification for function __gmpz_cmp
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __gmpz_clear
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
+tests/e-acsl-runtime/memsize.c:26:[value] Assertion got status invalid (stopping propagation).
+[value] done for function main
--
GitLab