diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
index 5a25bb7eacc937647c1c76bc769e186eed1243c7..49a7416378f37ac9841b79ccd938d5eec04958f6 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
@@ -384,8 +384,13 @@ void __init_argv(int argc, char **argv) {
}
}
-/* initialize contents of the abstract structure and record arguments */
-void __e_acsl_memory_init(int *argc_ref, char ***argv_ref) { }
+/* initialize contents of the abstract structure and record arguments
+ * argc_ref address the variable holding the argc parameter
+ * argv_ref address the variable holding the argv parameter
+ * ptr_size the size of the pointer computed during instrumentation. */
+void __e_acsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
+ arch_assert(ptr_size);
+}
/**********************/
/* DEBUG */
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
index 2eec3a56cb90735ed9fa631e22559699c3cb63da..9e0f59c4f9105916cd257dba9cd08d06e7214f69 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
@@ -87,4 +87,14 @@ static void runtime_assert(int predicate, char *kind,
void __e_acsl_assert(int pred, char *kind, char *fct, char *pred_txt, int line)
__attribute__ ((weak, alias ("runtime_assert")));
+/* Instances of assertions shared accross different memory models */
+
+/* Abort the execution if the size of the pointer computed during
+ * instrumentation (_ptr_sz) does not match the size of the pointer used
+ * by a compiler (void*) */
+#define arch_assert(_ptr_sz) \
+ vassert(_ptr_sz == sizeof(void*), \
+ "Mismatch of instrumentation- and compile-time pointer sizes: " \
+ "%lu vs %lu\n", _ptr_sz, sizeof(void*))
+
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index 75170c64f89a0b366d80e11c3b9209dd5113bcc1..4e72384efed52055760e3da7843e8a6338fa6d24 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
@@ -155,7 +155,7 @@ void __e_acsl_memory_clean(void)
/* initialize the abstract structure
* have to be called before any other statement in `main` */
/*@ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap; */
-void __e_acsl_memory_init(int *argc_ref, char ***argv)
+void __e_acsl_memory_init(int *argc_ref, char ***argv, size_t ptr_size)
__attribute__((FC_BUILTIN));
/* return the number of bytes dynamically allocated */
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
index 442d3f47cb9c3a98308755e0ef6508a5ddf8d404..41db747839a6f1ba1bbe5775fdae81d8af5f6d1a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
@@ -29,7 +29,7 @@ int main(void)
int __retres;
unsigned char buf[sizeof(union msg)];
int i;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(buf),16UL);
i = 0;
while ((unsigned long)i < sizeof(buf) / (unsigned long)4) {
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index b2ea1116c987439321b5cb79e401cd05af171aa3..27ae31be343713e9eb13409fc3d6df612d61749a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -216,7 +216,7 @@ int main(void)
float f;
float g;
float h;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& h),4UL);
__store_block((void *)(& g),4UL);
__store_block((void *)(& f),4UL);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index fdf7dd6b65aa34844d28b17dc63ab00f45f76107..e218608d3258d688d8ecedf5701fc8b1f8ca410f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -83,7 +83,7 @@ int main(void)
int __retres;
int t[7];
int n;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(t),28UL);
__initialize((void *)(t),sizeof(int));
t[0] = 1;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index 85f2b90c94b8e72f5968e100f7bf8052821dde26..67e2c8d506aa3b139cf16b61737262d73251e61d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -103,7 +103,7 @@ int main(void)
int __retres;
ArrayInt Accel;
int av;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& av),4UL);
__store_block((void *)(Accel),20UL);
__initialize((void *)(Accel),sizeof(int));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index b4bea7fed88c8f697a1186e740773c7299d82ba0..299751ff83cd69ea323249b92bd4fdd7f229adbd 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -184,7 +184,7 @@ void __e_acsl_globals_init(void)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
__e_acsl_memchr((void const *)__e_acsl_literal_string,'o',(unsigned long)4);
__e_acsl_memchr((void const *)__e_acsl_literal_string_2,'o',
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
index e243f9fc36fb87c0a66054d13b1f034139267cc6..8a94ba5b38d6586721c144c19a04cfc5622f46d5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -9,7 +9,7 @@ int main(void)
{
int __retres;
spongeState *state;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& state),8UL);
__full_init((void *)(& state));
state = (spongeState *)__e_acsl_malloc(sizeof(spongeState));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index fcb1c63d95e22deb1564a1b34f238696e151a7f5..b36de9b0ede568e37d44f07e8accb1cbe45b91b5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -44,7 +44,7 @@ void __e_acsl_globals_init(void)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
__e_acsl_loop();
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
index cdff0a19b958895c3bfdf5e4a16f82ca480ccdb8..1f7dcd91b0373d4e3f956ba15596cf84491d3257 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
@@ -7,7 +7,7 @@ int main(void)
int __retres;
struct toto s;
struct toto *p;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& p),8UL);
__store_block((void *)(& s),0UL);
/*@ assert \valid(&s); */
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index 80fffbde75da8971f08f0136ac61bd84778a519d..f925f71a738d55176ad79545741961ac8e82735d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -4,7 +4,7 @@ int main(void)
int __retres;
int a;
int *p;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& p),8UL);
__store_block((void *)(& a),4UL);
__full_init((void *)(& a));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
index 020ae8cae1fc9c899075f1456d0ab981cb858d1c..947d3ff3898b3cf86070b9a18fabf87284478ebe 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -4,7 +4,7 @@ int main(void)
int __retres;
int a;
int *p;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& p),8UL);
__store_block((void *)(& a),4UL);
__full_init((void *)(& a));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index 3575487d540b61efd8b5cb048545bf0e5298e2f5..8d8070a212c1ea55f9fd7b298c24c2e60d87c34d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -78,7 +78,7 @@ int main(void)
{
int __retres;
int i;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
i = 4;
while (1) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
index b9a4f8ec8efcb6bae068857a7091ec968c1232ed..71eb9845e69428bd287f67a9890fd0e2c178d6c6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
@@ -30,7 +30,7 @@ int main(void)
{
int __retres;
int x;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
x = 0;
f();
/*@ assert &x ≡ &x; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
index 8c932b2ee890f8a639bc02019929ce31cf0e12f8..4b3a9dd00736060482a81a064c6518fdb928ca1e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
@@ -17,7 +17,7 @@ int main(void)
{
int __retres;
int i;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& i),4UL);
f(& i,255);
/*@ assert \initialized(&i); */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
index ec503fdfcf7579c19091f667b90998dd9de8f21f..11d16adfb95a3cb347ea8c506d44c5e19fa0a63b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
@@ -38,7 +38,7 @@ int main(void)
int *p;
int *q;
int *r;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& q),8UL);
__store_block((void *)(& p),8UL);
__store_block((void *)(& x),4UL);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c
index 86de3ec5d8513ad91762ed3f8cda0e5c8dfbf7d7..e414f7e2244f5b09d6988b0c9bf309f221a37b64 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c
@@ -60,7 +60,7 @@ void __e_acsl_globals_init(void)
int main(int argc, char **argv)
{
int __retres;
- __e_acsl_memory_init(& argc,& argv);
+ __e_acsl_memory_init(& argc,& argv,8UL);
__e_acsl_globals_init();
/*@ assert \valid((char **)_A); */
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
index cfeb1f025b29221009313c2a1ee3f2539ce00223..533330efbb6a685ed53daaf312216e1bc5e7ccd7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
@@ -3,7 +3,7 @@ int main(void)
{
int __retres;
int *p;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& p),8UL);
/*@ assert ¬\freeable(p); */
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
index c315dd036e516e503acdbc8fba923c25d0c0a8d3..7ebafbc24c1c6bf2fe7709a0a3e58a8e94127cf0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
@@ -14,7 +14,7 @@ int main(void)
{
int __retres;
int *q;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
__store_block((void *)(& q),8UL);
P = & G;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
index 497d521190c52f8e81f627c43057464f8208b080..509bb30af842cbf1fb16ef1090c92d6476137110 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
@@ -15,7 +15,7 @@ int main(void)
int __retres;
int *p;
int *q;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
__store_block((void *)(& q),8UL);
__store_block((void *)(& p),8UL);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index 6fd0d619df3f1ce52eb6aeb10d4af0d1a163cffb..5103efe8310be07d85db51bc2636551a02e2474e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
@@ -58,7 +58,7 @@ int main(void)
{
int __retres;
char *SS;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
__store_block((void *)(& SS),8UL);
__full_init((void *)(& SS));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index 6332163e50dd7154b8d15af2ebffc780b7534ab7..0a35857a17a9b09365ed97ee8cce3855bd6bb426 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -38,7 +38,7 @@ int main(void)
{
int __retres;
struct list *l;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& l),8UL);
__full_init((void *)(& l));
l = (struct list *)0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index 10ef1b6904fed9886b444f996190386eed0e0d92..7a93e7c739707a43b21011b1c2e889ccc341f172 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -3,7 +3,7 @@ int main(int argc, char **argv)
{
int __retres;
int i;
- __e_acsl_memory_init(& argc,& argv);
+ __e_acsl_memory_init(& argc,& argv,8UL);
__init_argv(argc,argv);
/*@ assert \valid(&argc); */
{
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
index d11870325003374504e9e37ff368701e45157567..1cf25804fadab51454285e2f06eac95d7ef96327 100644
--- 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
@@ -4,7 +4,7 @@ int main(int argc, char **argv)
int __retres;
char *a;
char *b;
- __e_acsl_memory_init(& argc,& argv);
+ __e_acsl_memory_init(& argc,& argv,8UL);
__store_block((void *)(& b),8UL);
__store_block((void *)(& a),8UL);
__full_init((void *)(& a));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index 33227a516711a6e027e3aa496e2f88912d7b52c8..a5d213aa97917f1b1dd6f05533b8fd0b20a77a37 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -5,7 +5,7 @@ int main(void)
int x;
int t[3];
int *p;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& p),8UL);
__store_block((void *)(t),12UL);
__store_block((void *)(& x),4UL);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index 1335fd7a99d86933266658290d0ad9ad6e86c262..0b3e6de4726af6f5bf14c8d3982e6b68e3fbdb99 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
@@ -31,7 +31,7 @@ int main(void)
int __retres;
int *x;
int *y;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
__store_block((void *)(& y),8UL);
__store_block((void *)(& x),8UL);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
index c06645e065631f18f55699cf0d84ceb50e1be322..2f12c0aa0857aa093d8a0df1e222c99b884af843 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
@@ -21,7 +21,7 @@ int main(void)
int __retres;
FILE *f;
FILE *f2;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
__store_block((void *)(& f),8UL);
__full_init((void *)(& f));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index e020e1dc08d51b71a01fca664922fbab691aff4d..c3b7d26d52a678165abc605f73decc8a21e28753 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -123,7 +123,7 @@ int main(void)
int **c;
int ***d;
int n;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
__store_block((void *)(& n),4UL);
__store_block((void *)(& d),8UL);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index 8b9cd8c84b19ae4ab9cc3a9d23709f66b3a879c1..a9820f674bdfaf623f2b7751e2dbb66a06592882 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -5,7 +5,7 @@ int main(void)
int *a;
int *b;
int n;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& b),8UL);
__store_block((void *)(& a),8UL);
n = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index df39cdbf53c1e69c9bc5a7fc51c6da9fcc8617d9..c734d6606bb0552f3a35b4fa23a99554c0651950 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -107,7 +107,7 @@ struct list *__e_acsl_f(struct list *l)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_f((struct list *)0);
__retres = 0;
__e_acsl_memory_clean();
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index eafb9f7e38baf0d8f6f0fbd67f49ae70d148f878..c89a44fee1150ac525ee983d7fb724866eb22136 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -23,7 +23,7 @@ int main(void)
int x;
int v1[3];
int *v2;
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(& v2),8UL);
__store_block((void *)(v1),12UL);
x = 3;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index aa715235387c323d46ac36d45c2563875e57faed..32a3edd81ccc395dde770a2e3701a06da567c572 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -140,7 +140,7 @@ int main(void)
int __retres;
int x;
int t[2];
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(t),8UL);
__store_block((void *)(& x),4UL);
__full_init((void *)(& x));
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
index e9933d90555082a77c5f2c1a039cef8f0eb19c95..4ed21e95ef35f04002c3fdf34f2485ae4a2b9270 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -221,7 +221,7 @@ int main(void)
int __retres;
int x;
int t[2];
- __e_acsl_memory_init((int *)0,(char ***)0);
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
__store_block((void *)(t),8UL);
__store_block((void *)(& x),4UL);
__full_init((void *)(& x));
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 119f8d0914eb1e54d1297fa93c7bee7ea564370a..af39f0ae3196ff8bfc69bd38f8cb453224a08f7a 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -275,6 +275,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
match main_fct with
| Some main ->
let charPtrPtrType = TPtr(Cil.charPtrType,[]) in
+ let ptrSz = (Cil.sizeOf loc Cil.voidPtrType) in
let args =
(* Record arguments only if the first one has int type and the
second one is an array of char pointers of equivalent. This is
@@ -293,7 +294,8 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
initialization function, i.e., [__e_acsl_memory_init] *)
List.map Cil.mkAddrOfVi main.sformals;
| _ -> let null = Cil.integer loc 0
- in [ null ; null ] in
+ in [ null ; null ] in
+ let args = args @ [ptrSz] in
let init = Misc.mk_call
Location.unknown "__e_acsl_memory_init" args in
main.sbody.bstmts <- init :: main.sbody.bstmts;