diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 5f2eeba808130e5898056e194369e98dd2d15c78..71fa4565ae6dec2fa379c3184def1e4273bbe3dc 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,10 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2016/01/05] Fix bug in the memory model that caused the
+ tracked size of heap memory be computed incorrectly.
+- E-ACSL [2015/12/15] Added a convenience script for small runs of the
+ E-ACSL plugin.
-* E-ACSL [2015/08/12] Fix bug #1817 about incloorect initialization of
literal strings in global in arrays with compound initializers.
-* E-ACSL [2015/11/06] Fix a crash occuring when using a recent libc
diff --git a/src/plugins/e-acsl/gcc_test.sh b/src/plugins/e-acsl/gcc_test.sh
index 68809db7ecdd76b0d5c11d529fddd839b41c4932..3ec2e5b8f9646b1d9ee2f3f1097ba9124ef45c5e 100755
--- a/src/plugins/e-acsl/gcc_test.sh
+++ b/src/plugins/e-acsl/gcc_test.sh
@@ -9,10 +9,10 @@ if [ $# -gt 2 ]; then
ARGS=$@
fi
-gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
+gcc -std=c99 -Wall -Wno-unused-function -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
-# gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_list.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
+# gcc -std=c99 -Wall -Wno-unused-function -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_list.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
-# gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_splay_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
+# gcc -std=c99 -Wall -Wno-unused-function -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_splay_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
-# gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
+# gcc -std=c99 -Wall -Wno-unused-function -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index a3e786decd721da310af3bfd8ac5befb6d198754..dae2bc058f46bdb1c0fd7a49dc1fdf08737adbc0 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -52,13 +52,28 @@ SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,R,L,M,l:,e:,g,q,s:,F:"
# Prefix for an error message due to wrong arguments
ERROR="ERROR parsing arguments:"
+# Architecture-dependent flags. Since by default Frama-C uses 32-bit
+# architecture we need to make sure that same architecture is used for
+# instrumentation and for compilation.
+MACHDEPFLAGS="`getconf LONG_BIT`"
+# Check if getconf gives out the value accepted by Frama-C/GCC
+echo "$MACHDEPFLAGS" | grep '16\|32\|64' \
+ || error "$MACHDEPFLAGS-bit architecture not supported"
+# -machdep option sent to frama-c
+MACHDEP="-machdep gcc_x86_$MACHDEPFLAGS"
+# Macro for correct preprocessing of Frama-C generated code
+CPPMACHDEP="-D__FC_MACHDEP_X86_$MACHDEPFLAGS"
+# GCC machine option
+GCCMACHDEP="-m$MACHDEPFLAGS"
+
# Gcc
CC="`check_tool 'gcc'`"
-CFLAGS="-std=c99 -g3 -O2 -pedantic -fno-builtin -Wall \
+CFLAGS="-std=c99 $GCCMACHDEP -g3 -O2 -pedantic -fno-builtin -Wall \
-Wno-long-long \
-Wno-attributes \
-Wno-unused-result \
-Wno-unused-value \
+ -Wno-unused-function \
-Wno-unused-variable \
-Wno-unused-but-set-variable \
-Wno-implicit-function-declaration \
@@ -78,25 +93,6 @@ RTL="$EACSL_SHARE/e_acsl.c \
$EACSL_SHARE/memory_model/e_acsl_bittree.c \
"
-# Frama-c machdep option
-ARCH="$(uname -m | tr -d '\n')"
-case $ARCH in
- x86_64)
- MACHDEPFLAGS="86_64"
- ;;
- i686)
- MACHDEPFLAGS="86_32"
- ;;
- *)
- error "Unsupported archirtecture: $ARCH"
- ;;
-esac
-
-# -machdep option sent to frama-c
-MACHDEP="-machdep gcc_x$MACHDEPFLAGS"
-# Macro for correct preprocessing of Frama-C generated code
-CPPMACHDEP="-D__FC_MACHDEP_X$MACHDEPFLAGS"
-
# CPP and LD flags for compilation of E-ACSL-generated sources
EACSL_CPP_FLAGS="
-D__FC_errno=(*__errno_location())
@@ -122,7 +118,7 @@ OPTION_EXTRA_CPP="-I$FRAMA_C_SHARE/libc $CPPMACHDEP" # Extra CPP flags
manpage() {
echo "NAME"
- echo " e-acsl-gcc -- convenience wrapper instrumentation of C files with"
+ echo " e-acsl-gcc -- convenience wrapper for instrumentation of C files with"
echo " the E-ACSL Frama-C plugin and their subsequent compilation using"
echo " GNU compiler collection (GCC)"
echo ""
@@ -212,6 +208,7 @@ do
manpage;
;;
# Do not echo commands to STDOUT
+ # Set log and debug flags to minimal verbosity levels
--quiet|-q)
shift;
OPTION_ECHO=
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h
new file mode 100644
index 0000000000000000000000000000000000000000..126260ac88b4c67b6277165deb3e362cd1bbd6b1
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h
@@ -0,0 +1,315 @@
+/*
+ * Copyright (c) 2004,2012 Kustaa Nyholm / SpareTimeLabs
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without modification,
+ * are permitted provided that the following conditions are met:
+ *
+ * Redistributions of source code must retain the above copyright notice, this list
+ * of conditions and the following disclaimer.
+ *
+ * Redistributions in binary form must reproduce the above copyright notice, this
+ * list of conditions and the following disclaimer in the documentation and/or other
+ * materials provided with the distribution.
+ *
+ * Neither the name of the Kustaa Nyholm or SpareTimeLabs nor the names of its
+ * contributors may be used to endorse or promote products derived from this software
+ * without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+ * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
+ * IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT,
+ * INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
+ * NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA,
+ * OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
+ * WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY
+ * OF SUCH DAMAGE.
+ */
+
+#include <stdarg.h>
+#include <stddef.h>
+#include <stdint.h>
+#include <string.h>
+#include <unistd.h>
+#include <limits.h>
+
+// For PATH_MAX in Linux
+#ifdef __linux__
+ #include <linux/limits.h>
+#endif
+
+static void printf(char *fmt, ...);
+
+static void eprintf(char *fmt, ...);
+
+static void dprintf(int fd, char *fmt, ...);
+
+static void sprintf(char* s,char *fmt, ...);
+
+static void vabort(char *fmt, ...);
+
+typedef void (*putcf) (void*,char);
+
+static void uli2a(unsigned long int num, unsigned int base, int uc,char * bf) {
+ int n=0;
+ unsigned int d=1;
+ while (num/d >= base)
+ d*=base;
+ while (d!=0) {
+ int dgt = num / d;
+ num%=d;
+ d/=base;
+ if (n || dgt>0|| d==0) {
+ *bf++ = dgt+(dgt<10 ? '0' : (uc ? 'A' : 'a')-10);
+ ++n;
+ }
+ }
+ *bf=0;
+}
+
+static void li2a (long num, char * bf) {
+ if (num<0) {
+ num=-num;
+ *bf++ = '-';
+ }
+ uli2a(num,10,0,bf);
+}
+
+static void ui2a(unsigned int num, unsigned int base, int uc,char * bf) {
+ int n=0;
+ unsigned int d=1;
+ while (num/d >= base)
+ d*=base;
+ while (d!=0) {
+ int dgt = num / d;
+ num%= d;
+ d/=base;
+ if (n || dgt>0 || d==0) {
+ *bf++ = dgt+(dgt<10 ? '0' : (uc ? 'A' : 'a')-10);
+ ++n;
+ }
+ }
+ *bf=0;
+}
+
+static void i2a (int num, char * bf) {
+ if (num<0) {
+ num=-num;
+ *bf++ = '-';
+ }
+ ui2a(num,10,0,bf);
+}
+
+static int a2d(char ch) {
+ if (ch>='0' && ch<='9')
+ return ch-'0';
+ else if (ch>='a' && ch<='f')
+ return ch-'a'+10;
+ else if (ch>='A' && ch<='F')
+ return ch-'A'+10;
+ else return -1;
+}
+
+static char a2i(char ch, char** src,int base,int* nump) {
+ char* p= *src;
+ int num=0;
+ int digit;
+ while ((digit=a2d(ch))>=0) {
+ if (digit>base) break;
+ num=num*base+digit;
+ ch=*p++;
+ }
+ *src=p;
+ *nump=num;
+ return ch;
+}
+
+static void putchw(void* putp,putcf putf,int n, char z, char* bf) {
+ char fc=z? '0' : ' ';
+ char ch;
+ char* p=bf;
+ while (*p++ && n > 0)
+ n--;
+ while (n-- > 0)
+ putf(putp,fc);
+ while ((ch= *bf++))
+ putf(putp,ch);
+}
+
+static void putcp(void* p,char c) {
+ *(*((char**)p))++ = c;
+}
+
+static void _format(void* putp, putcf putf, char *fmt, va_list va) {
+ char bf[12];
+ char ch;
+ while ((ch=*(fmt++))) {
+ if (ch!='%')
+ putf(putp,ch);
+ else {
+ char lz=0;
+ char lng=0;
+ int w=0;
+ ch=*(fmt++);
+ if (ch=='0') {
+ ch=*(fmt++);
+ lz=1;
+ }
+ if (ch>='0' && ch<='9') {
+ ch=a2i(ch,&fmt,10,&w);
+ }
+ if (ch=='l') {
+ ch=*(fmt++);
+ lng=1;
+ }
+ switch (ch) {
+ case 0:
+ goto abort;
+ case 'u' : {
+ if (lng)
+ uli2a(va_arg(va, unsigned long int),10,0,bf);
+ else
+ ui2a(va_arg(va, unsigned int),10,0,bf);
+ putchw(putp,putf,w,lz,bf);
+ break;
+ }
+ case 'd': {
+ if (lng)
+ li2a(va_arg(va, unsigned long int),bf);
+ else
+ i2a(va_arg(va, int),bf);
+ putchw(putp,putf,w,lz,bf);
+ break;
+ }
+ case 'x':
+ case 'X':
+ if (lng)
+ uli2a(va_arg(va, unsigned long int),16,(ch=='X'),bf);
+ else
+ ui2a(va_arg(va, unsigned int),16,(ch=='X'),bf);
+ putchw(putp,putf,w,lz,bf);
+ break;
+ case 'f' : {
+ double num = va_arg(va, double);
+ int ord = (int)num;
+ i2a(ord,bf);
+ putchw(putp,putf,w,lz,bf);
+ putf(putp,'.');
+ num = num - ord;
+ num *= 1000;
+ ord = (int)num;
+ i2a(ord,bf);
+ putchw(putp,putf,w,lz,bf);
+ break;
+ }
+ case 'c' :
+ putf(putp,(char)(va_arg(va, int)));
+ break;
+ case 's' :
+ putchw(putp,putf,w,0,va_arg(va, char*));
+ break;
+ case '%' :
+ putf(putp,ch);
+ default:
+ break;
+ }
+ }
+ }
+abort:
+ ;
+}
+
+static void _charc_stdout (void* p, char c) { write(1,&c,1); }
+static void _charc_stderr (void* p, char c) { write(2,&c,1); }
+static void _charc_file (void* p, char c) { write((size_t)p,&c,1); }
+
+static void _charc_literal (void* p, char c) {
+ switch(c) {
+ case '\r':
+ write((size_t)p,"\\r",2);
+ break;
+ case '\f':
+ write((size_t)p,"\\f",2);
+ break;
+ case '\b':
+ write((size_t)p,"\\b",2);
+ break;
+ case '\a':
+ write((size_t)p,"\\a",2);
+ break;
+ case '\n':
+ write((size_t)p,"\\n",2);
+ break;
+ case '\t':
+ write((size_t)p,"\\t",2);
+ break;
+ case '\0':
+ write((size_t)p,"\\0",2);
+ break;
+ default:
+ write((size_t)p,&c,1);
+ }
+}
+
+static void printf(char *fmt, ...) {
+ va_list va;
+ va_start(va,fmt);
+ _format(NULL,_charc_stdout,fmt,va);
+ va_end(va);
+}
+
+static void eprintf(char *fmt, ...) {
+ va_list va;
+ va_start(va,fmt);
+ _format(NULL,_charc_stderr,fmt,va);
+ va_end(va);
+}
+
+static void vabort(char *fmt, ...) {
+ va_list va;
+ va_start(va,fmt);
+ _format(NULL,_charc_stderr,fmt,va);
+ va_end(va);
+ abort();
+}
+
+static void dprintf(int fd, char *fmt, ...) {
+ va_list va;
+ va_start(va,fmt);
+ intptr_t fd_long = fd;
+ _format((void*)fd_long,_charc_file,fmt,va);
+ va_end(va);
+}
+
+static void sprintf(char* s,char *fmt, ...) {
+ va_list va;
+ va_start(va,fmt);
+ _format(&s,putcp,fmt,va);
+ putcp(&s,0);
+ va_end(va);
+}
+
+#define assert(expr) \
+ ((expr) ? (void)(0) : vabort("%s at %s:%d\n", \
+ #expr, __FILE__,__LINE__))
+
+static void vassert_fail(int expr, int line, char *file, char *fmt, ...) {
+ if (!expr) {
+ char *afmt = "%s at %s:%d\n";
+ char buf [strlen(fmt) + strlen(afmt) + PATH_MAX + 11];
+ sprintf(buf, afmt, fmt, file, line);
+ fmt = buf;
+
+ va_list va;
+ va_start(va,fmt);
+ _format(NULL,_charc_stderr,fmt,va);
+ va_end(va);
+ abort();
+ }
+}
+
+#define vassert(expr, fmt, ...) \
+ vassert_fail(expr, __LINE__, __FILE__, fmt, __VA_ARGS__)
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
index 1ab256f0b6655b131a7bad31ad715881335ce8bb..b9d677e77a1ab5323bf5550e3b6f8a8b79fceca1 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
@@ -20,17 +20,15 @@
/* */
/**************************************************************************/
-#include <assert.h>
#include <errno.h>
#include <unistd.h>
-#include "stdio.h"
#include "stdlib.h"
#include "stdbool.h"
#include "math.h"
#include "e_acsl_mmodel_api.h"
#include "e_acsl_bittree.h"
#include "e_acsl_mmodel.h"
-
+#include "../e_acsl_printf.h"
#if WORDBITS == 16
@@ -50,11 +48,11 @@ const size_t Tmasks[] = {
0xfffff800,0xfffffc00,0xfffffe00,0xffffff00,0xffffff80,0xffffffc0,0xffffffe0,
0xfffffff0,0xfffffff8,0xfffffffc,0xfffffffe,0xffffffff};
-const int Teq[] =
+const int Teq[] =
{ 0,-1,3,-3,6,-5,7,-7,12,-9,11,-11,14,-13,15,-15,24,-17,19,-19,22,
-21,23,-23,28,-25,27,-27,30,-29,31,32,-32 };
-const int Tneq[] =
+const int Tneq[] =
{ 0,0,1,-2,2,-4,5,-6,4,-8,9,-10,10,-12,13,-14,8,-16,17,-18,18,-20,21,-22,20,
-24,25,-26,26,-28,29,-30,-31 };
@@ -79,12 +77,12 @@ const size_t Tmasks[] = {
0xfffffffffffffff8,0xfffffffffffffffc,0xfffffffffffffffe,0xffffffffffffffff};
-const int Teq[] =
+const int Teq[] =
{ 0,-1,3,-3,6,-5,7,-7,12,-9,11,-11,14,-13,15,-15,24,-17,19,-19,22,-21,23,-23,
28,-25,27,-27,30,-29,31,-31,48,-33,35,-35,38,-37,39,-39,44,-41,43,-43,46,
-45,47,-47,56,-49,51,-51,54,-53,55,-55,60,-57,59,-59,62,-61,63,64,-64 };
-const int Tneq[] =
+const int Tneq[] =
{ 0,0,1,-2,2,-4,5,-6,4,-8,9,-10,10,-12,13,-14,8,-16,17,-18,18,-20,21,-22,20,
-24,25,-26,26,-28,29,-30,16,-32,33,-34,34,-36,37,-38,36,-40,41,-42,42,-44,
45,-46,40,-48,49,-50,50,-52,53,-54,52,-56,57,-58,58,-60,61,-62,-63 };
@@ -113,7 +111,7 @@ size_t mask(size_t a, size_t b) {
size_t nxor = ~(a ^ b), ret;
int i = WORDBITS/2; /* dichotomic search, starting in the middle */
/*cpt_mask++;*/
-
+
/* if the current mask matches we use transition from Teq, else from Tneq
we stop as soon as i is negative, meaning that we found the mask
a negative element i from Teq or Tneq means stop and return Tmasks[-i] */
@@ -181,7 +179,7 @@ struct bittree * __get_leaf_from_block (struct _block * ptr) {
void __remove_element (struct _block * ptr) {
struct bittree * leaf_to_delete = __get_leaf_from_block (ptr);
assert(leaf_to_delete->leaf == ptr);
-
+
if(leaf_to_delete->father == NULL)
// the leaf is the root
__root = NULL;
@@ -251,7 +249,7 @@ struct bittree * __most_similar_node (struct _block * ptr) {
void __add_element (struct _block * ptr) {
struct bittree * new_leaf;
assert(ptr != NULL);
-
+
new_leaf = malloc(sizeof(struct bittree));
assert(new_leaf != NULL);
new_leaf->is_leaf = true;
@@ -266,7 +264,7 @@ void __add_element (struct _block * ptr) {
__root = new_leaf;
else {
struct bittree * brother = __most_similar_node (ptr), * father, * aux;
-
+
assert(brother != NULL);
father = malloc(sizeof(struct bittree));
assert(father != NULL);
@@ -282,7 +280,7 @@ void __add_element (struct _block * ptr) {
father->right = new_leaf;
}
new_leaf->father = father;
-
+
if(brother == __root) {
father->father = NULL;
father->mask = mask(brother->addr & brother->mask, ptr->ptr);
@@ -354,7 +352,7 @@ struct _block * __get_cont (void * ptr) {
struct bittree * t [WORDBITS];
short ind = -1;
-
+
while(1) {
if(tmp->is_leaf) {
/* tmp cannot contain ptr because its begin addr is higher */
@@ -381,7 +379,7 @@ struct _block * __get_cont (void * ptr) {
continue;
}
}
-
+
assert(tmp->left != NULL && tmp->right != NULL);
/* the right child has the highest address, so we test it first */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
index 3d18466210f7e63e0e6694864ad13ffad5ebb649..0211b04a65189fd727bfdfc17b24174ff4c86a54 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
@@ -20,45 +20,53 @@
/* */
/**************************************************************************/
-#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdbool.h>
-#include <assert.h>
#include "e_acsl_mmodel_api.h"
#include "e_acsl_mmodel.h"
+#include "../e_acsl_printf.h"
+// E-ACSL warnings {{{
+#define WARNING 0 // Output a warning message to stderr
+#define ERROR 1 // Treat warnings as errors and abort execution
+#define IGNORE 2 // Ignore warnings
-#define WARNING 0
-#define ERROR 1
-#define IGNORE 2
-
-
-#ifdef E_ACSL_WARNING
-int __warning_level = E_ACSL_WARNING;
-#else
-int __warning_level = WARNING;
+#ifndef E_ACSL_WARNING
+#define E_ACSL_WARNING WARNING
#endif
+static int warning_level = E_ACSL_WARNING;
-void __warning(const char* fct_name) {
- fprintf(stderr,
- "warning: E_ACSL function '%s' called with null pointer\n", fct_name);
+// Issue a warning to stderr or abort a program
+// based on the current warning level
+static void warning(const char* message) {
+ if (warning_level != IGNORE) {
+ eprintf("warning: %s\n", message);
+ if (warning_level == ERROR)
+ abort();
+ }
}
+// Shortcut for issuing a warning and returning from a function
+#define return_warning(_cond,_msg) \
+ if(_cond) { \
+ warning(_msg); \
+ return; \
+ }
+// }}}
-void* __e_acsl_mmodel_memset (void* dest, int val, size_t len) {
+void* __e_acsl_mmodel_memset(void* dest, int val, size_t len) {
unsigned char *ptr = (unsigned char*)dest;
while (len-- > 0)
*ptr++ = val;
return dest;
}
-
size_t __memory_size = 0;
/*unsigned cpt_store_block = 0;*/
-const int nbr_bits_to_1[256] = {
+static const int nbr_bits_to_1[256] = {
0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
};
@@ -73,11 +81,10 @@ size_t __get_memory_size(void) {
@ ensures size%8 == 0 ==> \result == size/8;
@ ensures size%8 != 0 ==> \result == size/8+1;
@*/
-size_t needed_bytes (size_t size) {
+static size_t needed_bytes (size_t size) {
return (size % 8) == 0 ? (size/8) : (size/8 + 1);
}
-
/* adds argc / argv to the memory model */
void __init_args(int argc, char **argv) {
int i;
@@ -112,9 +119,7 @@ void* __store_block(void* ptr, size_t size) {
/* remove the block starting at ptr */
void __delete_block(void* ptr) {
- struct _block * tmp;
- assert(ptr != NULL);
- tmp = __get_exact(ptr);
+ struct _block * tmp = __get_exact(ptr);
assert(tmp != NULL);
__clean_init(tmp);
__remove_element(tmp);
@@ -164,16 +169,15 @@ void* __realloc(void* ptr, size_t size) {
struct _block * tmp;
void * new_ptr;
if(ptr == NULL) return __malloc(size);
- if(size <= 0) {
- __memory_size -= __get_exact(ptr)->size;
+ if(size == 0) {
__free(ptr);
return NULL;
}
tmp = __get_exact(ptr);
- __memory_size -= tmp->size;
assert(tmp != NULL);
new_ptr = realloc((void*)tmp->ptr, size);
if(new_ptr == NULL) return NULL;
+ __memory_size -= tmp->size;
tmp->ptr = (size_t)new_ptr;
/* uninitialized, do nothing */
if(tmp->init_cpt == 0) ;
@@ -235,24 +239,16 @@ void __initialize (void * ptr, size_t size) {
struct _block * tmp;
unsigned i;
- if(ptr == NULL) {
- if(__warning_level == ERROR) assert(0);
- else if(__warning_level == IGNORE) return;
- else { __warning("initialize"); return; }
- }
-
+ return_warning(ptr == NULL, "initialize");
+
assert(size > 0);
tmp = __get_cont(ptr);
- if(tmp == NULL) {
- if(__warning_level == ERROR) assert(0);
- else if(__warning_level == IGNORE) return;
- else { __warning("initialize"); return; }
- }
-
+ return_warning(tmp == NULL, "initialize");
+
/* already fully initialized, do nothing */
if(tmp->init_cpt == tmp->size) return;
-
+
/* fully uninitialized */
if(tmp->init_cpt == 0) {
int nb = needed_bytes(tmp->size);
@@ -261,13 +257,13 @@ void __initialize (void * ptr, size_t size) {
}
for(i = 0; i < size; i++) {
- int byte_offset = (size_t)ptr - tmp->ptr + i;
+ int byte_offset = (size_t)ptr - tmp->ptr + i;
int ind = byte_offset / 8;
unsigned char mask_bit = 1U << (7 - (byte_offset % 8));
if((tmp->init_ptr[ind] & mask_bit) == 0) tmp->init_cpt++;
tmp->init_ptr[ind] |= mask_bit;
}
-
+
/* now fully initialized */
if(tmp->init_cpt == tmp->size) {
free(tmp->init_ptr);
@@ -278,68 +274,44 @@ void __initialize (void * ptr, size_t size) {
/* mark all bytes of ptr as initialized */
void __full_init (void * ptr) {
struct _block * tmp;
-
- if(ptr == NULL) {
- if(__warning_level == ERROR) assert(0);
- else if(__warning_level == IGNORE) return;
- else { __warning("full_init"); return; }
- }
+ return_warning(ptr == NULL, "full_init");
tmp = __get_exact(ptr);
-
- if(tmp == NULL) {
- if(__warning_level == ERROR) assert(0);
- else if(__warning_level == IGNORE) return;
- else { __warning("full_init"); return; }
- }
+ return_warning(tmp == NULL, "full_init");
if (tmp->init_ptr != NULL) {
free(tmp->init_ptr);
tmp->init_ptr = NULL;
}
-
+
tmp->init_cpt = tmp->size;
}
/* mark a block as litteral string */
void __literal_string (void * ptr) {
struct _block * tmp;
-
- if(ptr == NULL) {
- if(__warning_level == ERROR) assert(0);
- else if(__warning_level == IGNORE) return;
- else { __warning("literal_string"); return; }
- }
-
+ return_warning(ptr == NULL, "literal_string");
tmp = __get_exact(ptr);
-
- if(tmp == NULL) {
- if(__warning_level == ERROR) assert(0);
- else if(__warning_level == IGNORE) return;
- else { __warning("literal_string"); return; }
- }
-
+ return_warning(tmp == NULL, "literal_string");
tmp->is_litteral_string = true;
}
/* return whether the size bytes of ptr are initialized */
int __initialized (void * ptr, size_t size) {
- struct _block * tmp;
unsigned i;
- assert(ptr != NULL);
assert(size > 0);
- tmp = __get_cont(ptr);
+ struct _block * tmp = __get_cont(ptr);
if(tmp == NULL)
return false;
-
+
/* fully uninitialized */
if(tmp->init_cpt == 0) return false;
/* fully initialized */
if(tmp->init_cpt == tmp->size) return true;
-
+
for(i = 0; i < size; i++) {
/* if one byte is uninitialized */
- int byte_offset = (size_t)ptr - tmp->ptr + i;
+ int byte_offset = (size_t)ptr - tmp->ptr + i;
int ind = byte_offset / 8;
unsigned char mask_bit = 1U << (7 - (byte_offset % 8));
if((tmp->init_ptr[ind] & mask_bit) == 0) return false;
@@ -349,9 +321,7 @@ int __initialized (void * ptr, size_t size) {
/* return the length (in bytes) of the block containing ptr */
size_t __block_length(void* ptr) {
- struct _block * tmp;
- assert(ptr != NULL);
- tmp = __get_cont(ptr);
+ struct _block * tmp = __get_cont(ptr);
assert(tmp != NULL);
return tmp->size;
}
@@ -382,26 +352,20 @@ int __valid_read(void* ptr, size_t size) {
/* return the base address of the block containing ptr */
void* __base_addr(void* ptr) {
- struct _block * tmp;
- assert(ptr != NULL);
- tmp = __get_cont(ptr);
+ struct _block * tmp = __get_cont(ptr);
assert(tmp != NULL);
return (void*)tmp->ptr;
}
/* return the offset of ptr within its block */
int __offset(void* ptr) {
- struct _block * tmp;
- assert(ptr != NULL);
- tmp = __get_cont(ptr);
+ struct _block * tmp = __get_cont(ptr);
assert(tmp != NULL);
return ((size_t)ptr - tmp->ptr);
}
void __out_of_bound(void* ptr, _Bool flag) {
- struct _block * tmp;
- assert(ptr != NULL);
- tmp = __get_cont(ptr);
+ struct _block * tmp = __get_cont(ptr);
assert(tmp != NULL);
tmp->is_out_of_bound = flag;
}
@@ -414,14 +378,14 @@ void __out_of_bound(void* ptr, _Bool flag) {
void __print_block (struct _block * ptr) {
if (ptr != NULL) {
printf("%p; %zu Bytes; %slitteral; [init] : %li ",
- (char*)ptr->ptr, ptr->size,
- ptr->is_litteral_string ? "" : "not ", ptr->init_cpt);
+ (char*)ptr->ptr, ptr->size,
+ ptr->is_litteral_string ? "" : "not ", ptr->init_cpt);
if(ptr->init_ptr != NULL) {
unsigned i;
for(i = 0; i < ptr->size; i++) {
- int ind = i / 8;
- int one_bit = (unsigned)1 << (8 - (i % 8) - 1);
- printf("%i", (ptr->init_ptr[ind] & one_bit) != 0);
+ int ind = i / 8;
+ int one_bit = (unsigned)1 << (8 - (i % 8) - 1);
+ printf("%i", (ptr->init_ptr[ind] & one_bit) != 0);
}
}
printf("\n");
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 0000000000000000000000000000000000000000..1d630e2aaaf89d6702f8fddc863e07b13eb16385
--- /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 0000000000000000000000000000000000000000..d3d869e4813eb64f528b87bc33d461a9dffeebbe
--- /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 0000000000000000000000000000000000000000..1b8a9bb8400e14cb31286b9bccb1178774abd827
--- /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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
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 0000000000000000000000000000000000000000..4769e9abc329d64c3555173b0283bb8663baef4e
--- /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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
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 0000000000000000000000000000000000000000..b5e711cfb61c3f9c2cd5d263b53933de27f608b1
--- /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