From 8e00fc0e8ac560db2b34063c003cc9413dd7e471 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 19 Feb 2016 12:42:49 +0100
Subject: [PATCH] [RTL] Dynamic guard against compilation using different
pointer size
---
.../e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h | 9 +++++++--
src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h | 10 ++++++++++
src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_call.c | 2 +-
.../e-acsl-runtime/oracle/gen_compound_initializers.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_init.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_literal_string.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_valid_alias.c | 2 +-
.../e-acsl-runtime/oracle/gen_valid_in_contract.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/gen_at.c | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c | 2 +-
src/plugins/e-acsl/visit.ml | 4 +++-
35 files changed, 52 insertions(+), 35 deletions(-)
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 5a25bb7eacc..49a7416378f 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 2eec3a56cb9..9e0f59c4f91 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 75170c64f89..4e72384efed 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 442d3f47cb9..41db747839a 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 b2ea1116c98..27ae31be343 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 fdf7dd6b65a..e218608d325 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 85f2b90c94b..67e2c8d506a 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 b4bea7fed88..299751ff83c 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 e243f9fc36f..8a94ba5b38d 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 fcb1c63d95e..b36de9b0ede 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 cdff0a19b95..1f7dcd91b03 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 80fffbde75d..f925f71a738 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 020ae8cae1f..947d3ff3898 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 3575487d540..8d8070a212c 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 b9a4f8ec8ef..71eb9845e69 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 8c932b2ee89..4b3a9dd0073 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 ec503fdfcf7..11d16adfb95 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 86de3ec5d85..e414f7e2244 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 cfeb1f025b2..533330efbb6 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 c315dd036e5..7ebafbc24c1 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 497d521190c..509bb30af84 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 6fd0d619df3..5103efe8310 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 6332163e50d..0a35857a17a 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 10ef1b6904f..7a93e7c7397 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 d1187032500..1cf25804fad 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 33227a51671..a5d213aa979 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 1335fd7a99d..0b3e6de4726 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 c06645e0656..2f12c0aa085 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 e020e1dc08d..c3b7d26d52a 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 8b9cd8c84b1..a9820f674bd 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 df39cdbf53c..c734d6606bb 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 eafb9f7e38b..c89a44fee11 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 aa715235387..32a3edd81cc 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 e9933d90555..4ed21e95ef3 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 119f8d0914e..af39f0ae319 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;
--
GitLab