diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index 3ba67aa2b869f4f6fccb0cfa3e651227e06b897d..d9adb77a2ce0dcedd723d3c95ab522bd6a41598a 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
@@ -221,7 +221,7 @@ static int allocated(void* ptr, size_t size, void *ptr_base) {
}
/* return whether the size bytes of ptr are readable/writable */
-static int valid(void* ptr, size_t size, void *ptr_base) {
+static int valid(void* ptr, size_t size, void *ptr_base, void *addr_of_base) {
/* Many similarities with allocated (so far at least), but it is better
* to use this tandalone definition, otherwise the block needs to be looked
* up twice */
@@ -233,7 +233,7 @@ static int valid(void* ptr, size_t size, void *ptr_base) {
}
/* return whether the size bytes of ptr are readable */
-static int valid_read(void* ptr, size_t size, void *ptr_base) {
+static int valid_read(void* ptr, size_t size, void *ptr_base, void *addr_of_base) {
return allocated(ptr, size, ptr_base);
}
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 858747bfe9dac07ba014203e8d757b3009606d6d..771b9bb47af9f9896bf660f7c7a4685398369412 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
@@ -134,7 +134,7 @@ int __e_acsl_freeable(void * ptr)
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
-int __e_acsl_valid(void * ptr, size_t size, void *ptr_base)
+int __e_acsl_valid(void * ptr, size_t size, void *ptr_base, void *addr_of_base)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\valid_read predicate of E-ACSL.
@@ -144,7 +144,7 @@ int __e_acsl_valid(void * ptr, size_t size, void *ptr_base)
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid_read(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
-int __e_acsl_valid_read(void * ptr, size_t size, void *ptr_base)
+int __e_acsl_valid_read(void * ptr, size_t size, void *ptr_base, void *addr_of_base)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\base_addr predicate of E-ACSL.
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
index 589d446bc574fcd4f018a2f5467d2929f25b5e9e..8ef1e350f1ea39e52a6a38a5d8c8e7dd1129effc 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
@@ -30,8 +30,8 @@
#include <errno.h>
#include <sys/resource.h>
-static int valid(void*, size_t, void*);
-static int valid_read(void*, size_t, void*);
+static int valid(void*, size_t, void*, void*);
+static int valid_read(void*, size_t, void*, void*);
#include "e_acsl_string.h"
#include "e_acsl_bits.h"
@@ -77,7 +77,7 @@ static void mark_readonly(void * ptr) {
/* E-ACSL annotations */
/* ****************** */
-static int valid(void * ptr, size_t size, void *ptr_base) {
+static int valid(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
uintptr_t addr = (uintptr_t)ptr;
uintptr_t base = (uintptr_t)ptr_base;
if (IS_ON_HEAP(addr))
@@ -91,7 +91,7 @@ static int valid(void * ptr, size_t size, void *ptr_base) {
return 0;
}
-static int valid_read(void * ptr, size_t size, void *ptr_base) {
+static int valid_read(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
uintptr_t addr = (uintptr_t)ptr;
uintptr_t base = (uintptr_t)ptr_base;
TRY_SEGMENT_WEAK(addr,
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 610b8b71808a5898fc04c389312ed66ed4b03e80..5717cea664861ca0917acd17d42a8851651ba87e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -122,15 +122,17 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_store_block((void *)(& Mwmin),(size_t)8);
__e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
__gen_e_acsl_valid = __e_acsl_valid((void *)Mtmin_in,sizeof(float),
- (void *)Mtmin_in);
+ (void *)Mtmin_in,
+ (void *)(& Mtmin_in));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"bar",
(char *)"\\valid(Mtmin_in)",17);
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)Mwmin,sizeof(float),
- (void *)Mwmin);
+ (void *)Mwmin,(void *)(& Mwmin));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Precondition",
(char *)"bar",(char *)"\\valid(Mwmin)",18);
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmin_out,sizeof(float),
- (void *)Mtmin_out);
+ (void *)Mtmin_out,
+ (void *)(& Mtmin_out));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"bar",(char *)"\\valid(Mtmin_out)",19);
__gen_e_acsl_at_6 = Mwmin;
@@ -148,12 +150,14 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __gen_e_acsl_if;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
sizeof(float),
- (void *)__gen_e_acsl_at_2);
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",23);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
sizeof(float),
- (void *)__gen_e_acsl_at);
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",23);
if (*__gen_e_acsl_at == *__gen_e_acsl_at_2) {
@@ -161,13 +165,15 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __gen_e_acsl_valid_read_4;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at_4,
sizeof(float),
- (void *)__gen_e_acsl_at_4);
+ (void *)__gen_e_acsl_at_4,
+ (void *)(& __gen_e_acsl_at_4));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_4)",
23);
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
sizeof(float),
- (void *)__gen_e_acsl_at_3);
+ (void *)__gen_e_acsl_at_3,
+ (void *)(& __gen_e_acsl_at_3));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_3)",
23);
@@ -178,7 +184,8 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __gen_e_acsl_valid_read_5;
__gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)__gen_e_acsl_at_5,
sizeof(float),
- (void *)__gen_e_acsl_at_5);
+ (void *)__gen_e_acsl_at_5,
+ (void *)(& __gen_e_acsl_at_5));
__e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_5)",
23);
@@ -188,7 +195,8 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __gen_e_acsl_valid_read_6;
__gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)__gen_e_acsl_at_6,
sizeof(float),
- (void *)__gen_e_acsl_at_6);
+ (void *)__gen_e_acsl_at_6,
+ (void *)(& __gen_e_acsl_at_6));
__e_acsl_assert(__gen_e_acsl_valid_read_6,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_6)",
23);
@@ -227,15 +235,17 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_store_block((void *)(& Mwmax),(size_t)8);
__e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
__gen_e_acsl_valid = __e_acsl_valid((void *)Mtmax_in,sizeof(float),
- (void *)Mtmax_in);
+ (void *)Mtmax_in,
+ (void *)(& Mtmax_in));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"foo",
(char *)"\\valid(Mtmax_in)",5);
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)Mwmax,sizeof(float),
- (void *)Mwmax);
+ (void *)Mwmax,(void *)(& Mwmax));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Precondition",
(char *)"foo",(char *)"\\valid(Mwmax)",6);
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmax_out,sizeof(float),
- (void *)Mtmax_out);
+ (void *)Mtmax_out,
+ (void *)(& Mtmax_out));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
(char *)"foo",(char *)"\\valid(Mtmax_out)",7);
__gen_e_acsl_at_3 = Mwmax;
@@ -249,17 +259,20 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
sizeof(float),
- (void *)__gen_e_acsl_at_3);
+ (void *)__gen_e_acsl_at_3,
+ (void *)(& __gen_e_acsl_at_3));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_3)",11);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
sizeof(float),
- (void *)__gen_e_acsl_at_2);
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",11);
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
sizeof(float),
- (void *)__gen_e_acsl_at);
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",11);
__e_acsl_assert(*__gen_e_acsl_at == *__gen_e_acsl_at_2 + ((long double)5 -
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 4bc40ad3c96d7f54390ffcfc69bb343154bc7439..04cb8cbdf7534223386e6d7ad5e7ab96680c50fc 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -67,7 +67,8 @@ int __gen_e_acsl_sorted(int *t, int n)
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + __gen_e_acsl_i),
- sizeof(int),(void *)t);
+ sizeof(int),(void *)t,
+ (void *)(& t));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
(char *)"sorted",
(char *)"mem_access: \\valid_read(t + __gen_e_acsl_i)",
@@ -75,7 +76,8 @@ int __gen_e_acsl_sorted(int *t, int n)
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (
__gen_e_acsl_i - 1L)),
sizeof(int),
- (void *)t);
+ (void *)t,
+ (void *)(& t));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"sorted",
(char *)"mem_access: \\valid_read(t + (long)(__gen_e_acsl_i - 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 a43f77b2940ecfd928efa7de9de121623553d58d..3473eaa5490140ed4885fad4d5f0853f8b8028f2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -80,13 +80,15 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
int __gen_e_acsl_valid_read_6;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(*__gen_e_acsl_at_6),
sizeof(int),
- (void *)(*__gen_e_acsl_at_6));
+ (void *)(*__gen_e_acsl_at_6),
+ (void *)__gen_e_acsl_at_6);
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read((int *)*__gen_e_acsl_at_6)",
8);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_5)[1]),
sizeof(int),
+ (void *)(& (*__gen_e_acsl_at_5)[1]),
(void *)(& (*__gen_e_acsl_at_5)[1]));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
@@ -94,6 +96,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
8);
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_4)[2]),
sizeof(int),
+ (void *)(& (*__gen_e_acsl_at_4)[2]),
(void *)(& (*__gen_e_acsl_at_4)[2]));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
@@ -101,6 +104,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
8);
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_3)[3]),
sizeof(int),
+ (void *)(& (*__gen_e_acsl_at_3)[3]),
(void *)(& (*__gen_e_acsl_at_3)[3]));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
@@ -108,6 +112,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
8);
__gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_2)[4]),
sizeof(int),
+ (void *)(& (*__gen_e_acsl_at_2)[4]),
(void *)(& (*__gen_e_acsl_at_2)[4]));
__e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
@@ -115,7 +120,8 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
8);
__gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
sizeof(int),
- (void *)__gen_e_acsl_at);
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
__e_acsl_assert(__gen_e_acsl_valid_read_6,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",8);
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 c12281a0ba6bf200678ac8e2e177d8bb06a47925..d162a6aa8af1d3950d49a402bad992c1dd71b1b4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -87,7 +87,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_k),
sizeof(char),
- (void *)buf);
+ (void *)buf,
+ (void *)(& buf));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)buf + __gen_e_acsl_k)",
@@ -116,7 +117,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_i),
sizeof(char),
- (void *)buf);
+ (void *)buf,
+ (void *)(& buf));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)buf + __gen_e_acsl_i)",
@@ -154,7 +156,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j),
sizeof(char),
- (void *)__gen_e_acsl_at_2);
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j)",
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 3590caabae6aeedcdb30157eeb98d26b1722a1d8..6e3a6dfa88ee40d0fd1d3c907dee3889c686d5da 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -30,7 +30,8 @@ void __gen_e_acsl_loop(void)
__e_acsl_assert(global_i == 0,(char *)"Precondition",(char *)"loop",
(char *)"global_i == 0",9);
__gen_e_acsl_valid = __e_acsl_valid((void *)global_i_ptr,sizeof(int),
- (void *)global_i_ptr);
+ (void *)global_i_ptr,
+ (void *)(& global_i_ptr));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"loop",
(char *)"\\valid(global_i_ptr)",10);
__e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition",
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 131275e9b9f51d014587a2c94a23df25fa2c2d5c..46cdc40280b2a41bae5d00081e7f4412322561ba 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
@@ -16,7 +16,7 @@ int main(void)
{
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)(& s),sizeof(struct toto),
- (void *)(& s));
+ (void *)(& s),(void *)(& s));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&s)",9);
}
@@ -33,7 +33,7 @@ int main(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(struct toto),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and = 0;
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 eb7b67ff6db71159d66ac56db65873e14f0ac4ce..438fc89ebd27fdcb880c09bfddb5df7fc4616b6e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -21,7 +21,7 @@ int main(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
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 a5539fcdbb00f4bff44442a4d3b692a4441c57c1..7da27f795d1a23f10e17960afb1913f2fda525bb 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -21,7 +21,7 @@ int main(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
index 2cde08d55325a6c7863a3b9e33cfc05dfcf7695e..b8abc7855dea64e3c0fa98e68fb90787f85a4998 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
@@ -22,7 +22,7 @@ int main(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -46,7 +46,7 @@ int main(void)
int __gen_e_acsl_valid_2;
/*@ assert Value: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
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 d897bb4bd4f495243bed735f0730e5356c77cc78..091b718682b1aec51686013c7921c2b027c8de4e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -18,7 +18,7 @@ int f(void)
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)S,sizeof(char),
- (void *)S);
+ (void *)S,(void *)(& S));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"Assertion",
(char *)"f",(char *)"\\valid_read(S)",10);
}
@@ -34,7 +34,8 @@ int f(void)
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)s1,
sizeof(char),
- (void *)s1);
+ (void *)s1,
+ (void *)(& s1));
__gen_e_acsl_and = __gen_e_acsl_valid_read_2;
}
else __gen_e_acsl_and = 0;
@@ -53,7 +54,8 @@ int f(void)
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)s2,
sizeof(char),
- (void *)s2);
+ (void *)s2,
+ (void *)(& s2));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_read_3;
}
else __gen_e_acsl_and_2 = 0;
@@ -116,7 +118,8 @@ int main(void)
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)s,
sizeof(char),
- (void *)s);
+ (void *)s,
+ (void *)(& s));
__gen_e_acsl_and = __gen_e_acsl_valid_read;
}
else __gen_e_acsl_and = 0;
@@ -134,7 +137,7 @@ int main(void)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)s,sizeof(char),
- (void *)s);
+ (void *)s,(void *)(& s));
__gen_e_acsl_and_2 = __gen_e_acsl_valid;
}
else __gen_e_acsl_and_2 = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
index 7fc2ab8fc6d7db6c8532765f734c674119654819..0e77c02a4decf4af5dddd66cbef446b6f3db413d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
@@ -42,7 +42,8 @@ int main(int argc, char **argv)
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_G[0].str,
sizeof(char),
- (void *)_G[0].str);
+ (void *)_G[0].str,
+ (void *)(& _G[0].str));
__gen_e_acsl_and = __gen_e_acsl_valid_read;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
index 62e95d5c96db776e94c19a54722c271e8c75dd87..39cb7d09423e9f44d7f2f27403f83fd890f087ad 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -39,7 +39,8 @@ int main(void)
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(srcbuf + i),
sizeof(char),
- (void *)srcbuf);
+ (void *)srcbuf,
+ (void *)(& srcbuf));
__e_acsl_assert(! __gen_e_acsl_valid_read,(char *)"Assertion",
(char *)"main",(char *)"!\\valid_read(srcbuf + i)",
16);
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 199148e05ca74735b293f3117d2af34b090fdd4e..3064cfc7f3ee3e36308d8a23acd57e189970e5b8 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -50,7 +50,8 @@ void g(int *p, int *q)
{
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,
+ (void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",28);
__gen_e_acsl_at_3 = *q;
@@ -58,7 +59,7 @@ void g(int *p, int *q)
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,(void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",26);
__gen_e_acsl_at = *q;
@@ -73,7 +74,8 @@ void g(int *p, int *q)
{
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
- sizeof(int),(void *)p);
+ sizeof(int),(void *)p,
+ (void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
26);
@@ -90,7 +92,8 @@ void g(int *p, int *q)
int __gen_e_acsl_valid_read_4;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at_3),
sizeof(int),
- (void *)p);
+ (void *)p,
+ (void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p + __gen_e_acsl_at_3)",
28);
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 21f713f783bfb6583e45dcdf079386e872f96cec..832354a78aa7c3b9a7165766abfc17b58e1206e8 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -107,7 +107,8 @@ void g(int *p, int *q)
{
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,
+ (void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",28);
__gen_e_acsl_at_3 = *q;
@@ -115,7 +116,7 @@ void g(int *p, int *q)
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,(void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",26);
__gen_e_acsl_at = *q;
@@ -131,7 +132,8 @@ void g(int *p, int *q)
int __gen_e_acsl_valid_read_2;
__e_acsl_mpz_t __gen_e_acsl_;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
- sizeof(int),(void *)p);
+ sizeof(int),(void *)p,
+ (void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
26);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
index 1797dace2f66c6c571b097d8eb344a25e86db6a9..7bf4aedf27fb3465b8acd51f9b552ebadadc0904 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
@@ -222,6 +222,7 @@ int main(void)
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i]),
sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i]),
(void *)(& buf[__gen_e_acsl_i]));
if (__gen_e_acsl_valid) ;
else {
@@ -251,6 +252,7 @@ int main(void)
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_2]),
sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_2]),
(void *)(& buf[__gen_e_acsl_i_2]));
if (__gen_e_acsl_valid_2) ;
else {
@@ -280,6 +282,7 @@ int main(void)
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_3]),
sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_3]),
(void *)(& buf[__gen_e_acsl_i_3]));
if (__gen_e_acsl_valid_3) ;
else {
@@ -326,6 +329,7 @@ int main(void)
__gen_e_acsl_i_5 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_4));
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_5]),
sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_5]),
(void *)(& buf[__gen_e_acsl_i_5]));
if (__gen_e_acsl_valid_4) ;
else {
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
index 1624bf0bb6999ed5faefa4ded29e71c53da07f69..a6bd697b3a406d685d1d35e68821b148f72b8b00 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
@@ -643,6 +643,7 @@ int main(void)
__gen_e_acsl_i_2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i));
__gen_e_acsl_valid = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_2]),
sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_2]),
(void *)(& buf[__gen_e_acsl_i_2]));
if (__gen_e_acsl_valid) ;
else {
@@ -702,6 +703,7 @@ int main(void)
__gen_e_acsl_i_4 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3));
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_4]),
sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_4]),
(void *)(& buf[__gen_e_acsl_i_4]));
if (__gen_e_acsl_valid_2) ;
else {
@@ -761,6 +763,7 @@ int main(void)
__gen_e_acsl_i_6 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_5));
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_6]),
sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_6]),
(void *)(& buf[__gen_e_acsl_i_6]));
if (__gen_e_acsl_valid_3) ;
else {
@@ -820,6 +823,7 @@ int main(void)
__gen_e_acsl_i_8 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_7));
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_8]),
sizeof(int),
+ (void *)(& buf[__gen_e_acsl_i_8]),
(void *)(& buf[__gen_e_acsl_i_8]));
if (__gen_e_acsl_valid_4) ;
else {
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
index 78019fc6e93d39db0abd3d2cb437075ceb0bdc7d..d52be564121ca61dc821df1d1de213a1344ca949 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
@@ -45,7 +45,8 @@ int main(int argc, char **argv)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -58,7 +59,7 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)(p + 1),sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__e_acsl_assert(! __gen_e_acsl_valid_2,(char *)"Assertion",
(char *)"main",(char *)"!\\valid(p + 1)",26);
}
@@ -75,7 +76,7 @@ int main(int argc, char **argv)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_2 = 0;
@@ -88,7 +89,7 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_4;
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)(p + 1),sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__e_acsl_assert(! __gen_e_acsl_valid_4,(char *)"Assertion",
(char *)"main",(char *)"!\\valid(p + 1)",31);
}
@@ -128,7 +129,7 @@ int main(int argc, char **argv)
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_5;
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)pmin,sizeof(char),
- (void *)pmin);
+ (void *)pmin,(void *)(& pmin));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_3 = 0;
@@ -146,7 +147,7 @@ int main(int argc, char **argv)
if (__gen_e_acsl_initialized_4) {
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)pmax,sizeof(char),
- (void *)pmax);
+ (void *)pmax,(void *)(& pmax));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_6;
}
else __gen_e_acsl_and_4 = 0;
@@ -159,7 +160,8 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_7;
__gen_e_acsl_valid_7 = __e_acsl_valid((void *)(pmin + diff),
- sizeof(char),(void *)pmin);
+ sizeof(char),(void *)pmin,
+ (void *)(& pmin));
__e_acsl_assert(! __gen_e_acsl_valid_7,(char *)"Assertion",
(char *)"main",(char *)"!\\valid(pmin + diff)",52);
}
@@ -169,7 +171,8 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_8;
__gen_e_acsl_valid_8 = __e_acsl_valid((void *)(pmax - diff),
- sizeof(char),(void *)pmax);
+ sizeof(char),(void *)pmax,
+ (void *)(& pmax));
__e_acsl_assert(! __gen_e_acsl_valid_8,(char *)"Assertion",
(char *)"main",(char *)"!\\valid(pmax - diff)",54);
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
index 3fbdf9ac552a4211b516738f365dd59c5b50dddb..846dc1d3a80244de0cc3eb891f0990355790de1f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
@@ -17,7 +17,7 @@ int main(int argc, char const **argv)
{
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)(& p),sizeof(int *),
- (void *)(& p));
+ (void *)(& p),(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",
(char *)"main",(char *)"\\valid(&p)",13);
__e_acsl_delete_block((void *)(& p));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
index 14230fde4888d75b2309ed5ac106369a087fc302..057ea447994508053d2f856124facf9f756e50d6 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
@@ -69,7 +69,7 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)(_A),sizeof(char *),
- (void *)(_A));
+ (void *)(_A),(void *)(& _A));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid((char **)_A)",33);
}
@@ -85,7 +85,8 @@ int main(int argc, char **argv)
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_A[0],
sizeof(char),
- (void *)_A[0]);
+ (void *)_A[0],
+ (void *)(_A));
__gen_e_acsl_and = __gen_e_acsl_valid_read;
}
else __gen_e_acsl_and = 0;
@@ -104,7 +105,8 @@ int main(int argc, char **argv)
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)_A[1],
sizeof(char),
- (void *)_A[1]);
+ (void *)_A[1],
+ (void *)(& _A[1]));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_read_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -118,7 +120,8 @@ int main(int argc, char **argv)
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)_B,
sizeof(char),
- (void *)_B);
+ (void *)_B,
+ (void *)(& _B));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"Assertion",
(char *)"main",(char *)"\\valid_read(_B)",36);
}
@@ -128,7 +131,7 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& _C),sizeof(char *),
- (void *)(& _C));
+ (void *)(& _C),(void *)(& _C));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
(char *)"main",(char *)"\\valid(&_C)",37);
}
@@ -138,7 +141,7 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)(_D),sizeof(int),
- (void *)(_D));
+ (void *)(_D),(void *)(& _D));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Assertion",
(char *)"main",(char *)"\\valid((int *)_D)",38);
}
@@ -148,7 +151,7 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_4;
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& _E),sizeof(int),
- (void *)(& _E));
+ (void *)(& _E),(void *)(& _E));
__e_acsl_assert(__gen_e_acsl_valid_4,(char *)"Assertion",
(char *)"main",(char *)"\\valid(&_E)",39);
}
@@ -158,7 +161,7 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_5;
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)(& _F),sizeof(int),
- (void *)(& _F));
+ (void *)(& _F),(void *)(& _F));
__e_acsl_assert(__gen_e_acsl_valid_5,(char *)"Assertion",
(char *)"main",(char *)"\\valid(&_F)",40);
}
@@ -172,7 +175,7 @@ int main(int argc, char **argv)
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)(& _G),
sizeof(struct ST [2]),
- (void *)(& _G));
+ (void *)(& _G),(void *)(& _G));
__e_acsl_assert(__gen_e_acsl_valid_6,(char *)"Assertion",
(char *)"main",(char *)"\\valid(&_G)",42);
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
index ebed0fabf70ee41539eddf7688152efdd45bb24a..310b358cf5159744fedd7994a9e44a833851e0d8 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
@@ -22,7 +22,8 @@ int main(int argc, char const **argv)
sizeof(char *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)d,sizeof(char),(void *)d);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)d,sizeof(char),(void *)d,
+ (void *)(& d));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
index 4403c92864139f487ad693cb4c69bb2f1184d8b0..03b3f2eac69e463438e7c0c509907a6dcdbbcc16 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
@@ -21,7 +21,7 @@ int goto_bts(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -45,7 +45,7 @@ int goto_bts(void)
int __gen_e_acsl_valid_2;
/*@ assert Value: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -112,7 +112,7 @@ int goto_valid(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -131,7 +131,7 @@ int goto_valid(void)
int __gen_e_acsl_valid_2;
/*@ assert Value: dangling_pointer: ¬\dangling(&q); */
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -150,7 +150,7 @@ int goto_valid(void)
int __gen_e_acsl_valid_3;
/*@ assert Value: dangling_pointer: ¬\dangling(&r); */
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)r,sizeof(int),
- (void *)r);
+ (void *)r,(void *)(& r));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_3 = 0;
@@ -182,7 +182,7 @@ int goto_valid(void)
int __gen_e_acsl_valid_4;
/*@ assert Value: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_4 = 0;
@@ -201,7 +201,7 @@ int goto_valid(void)
int __gen_e_acsl_valid_5;
/*@ assert Value: dangling_pointer: ¬\dangling(&q); */
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_5 = 0;
@@ -220,7 +220,7 @@ int goto_valid(void)
int __gen_e_acsl_valid_6;
/*@ assert Value: dangling_pointer: ¬\dangling(&r); */
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)r,sizeof(int),
- (void *)r);
+ (void *)r,(void *)(& r));
__gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
}
else __gen_e_acsl_and_6 = 0;
@@ -273,7 +273,7 @@ int switch_valid(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -291,7 +291,7 @@ int switch_valid(void)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -309,7 +309,7 @@ int switch_valid(void)
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)s,sizeof(int),
- (void *)s);
+ (void *)s,(void *)(& s));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_3 = 0;
@@ -344,7 +344,7 @@ int switch_valid(void)
int __gen_e_acsl_valid_4;
/*@ assert Value: dangling_pointer: ¬\dangling(&q); */
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_4 = 0;
@@ -363,7 +363,7 @@ int switch_valid(void)
int __gen_e_acsl_valid_5;
/*@ assert Value: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_5 = 0;
@@ -381,7 +381,7 @@ int switch_valid(void)
if (__gen_e_acsl_initialized_6) {
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)s,sizeof(int),
- (void *)s);
+ (void *)s,(void *)(& s));
__gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
}
else __gen_e_acsl_and_6 = 0;
@@ -438,7 +438,7 @@ int while_valid(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -456,7 +456,8 @@ int while_valid(void)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,
+ (void *)(& q));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -474,7 +475,8 @@ int while_valid(void)
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)r,sizeof(int),
- (void *)r);
+ (void *)r,
+ (void *)(& r));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_3 = 0;
@@ -504,7 +506,7 @@ int while_valid(void)
/*@ assert Value: initialisation: \initialized(&p); */
/*@ assert Value: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_4 = 0;
@@ -524,7 +526,7 @@ int while_valid(void)
/*@ assert Value: initialisation: \initialized(&q); */
/*@ assert Value: dangling_pointer: ¬\dangling(&q); */
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_5 = 0;
@@ -542,7 +544,7 @@ int while_valid(void)
if (__gen_e_acsl_initialized_6) {
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)r,sizeof(int),
- (void *)r);
+ (void *)r,(void *)(& r));
__gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
}
else __gen_e_acsl_and_6 = 0;
@@ -585,7 +587,7 @@ void continue_valid(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -603,7 +605,7 @@ void continue_valid(void)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -626,7 +628,7 @@ void continue_valid(void)
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_3 = 0;
@@ -644,7 +646,7 @@ void continue_valid(void)
if (__gen_e_acsl_initialized_4) {
int __gen_e_acsl_valid_4;
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_4 = 0;
@@ -668,7 +670,7 @@ void continue_valid(void)
if (__gen_e_acsl_initialized_5) {
int __gen_e_acsl_valid_5;
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_5 = 0;
@@ -687,7 +689,7 @@ void continue_valid(void)
if (__gen_e_acsl_initialized_6) {
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
}
else __gen_e_acsl_and_6 = 0;
@@ -718,7 +720,7 @@ void continue_valid(void)
if (__gen_e_acsl_initialized_7) {
int __gen_e_acsl_valid_7;
__gen_e_acsl_valid_7 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_7 = __gen_e_acsl_valid_7;
}
else __gen_e_acsl_and_7 = 0;
@@ -736,7 +738,7 @@ void continue_valid(void)
if (__gen_e_acsl_initialized_8) {
int __gen_e_acsl_valid_8;
__gen_e_acsl_valid_8 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q);
+ (void *)q,(void *)(& q));
__gen_e_acsl_and_8 = __gen_e_acsl_valid_8;
}
else __gen_e_acsl_and_8 = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
index 1c54b9a880e53a10fd4b75d7d4424ce7d0b196d8..9cb07642279390e855785d910bab99adab7ba204 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
@@ -26,7 +26,8 @@ int main(int argc, char const **argv)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
index 9854490a0ccf6ba17f73c5bc86e110ea45ff045a..8adeba00d7ff1c5ac395702ae11d4cae52355ae4 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
@@ -17,7 +17,8 @@ void f(void)
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(T + G),
- sizeof(char),(void *)T);
+ sizeof(char),(void *)T,
+ (void *)(& T));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
(char *)"mem_access: \\valid_read(T + G)",11);
__e_acsl_assert(*(T + G) == 'b',(char *)"Assertion",(char *)"f",
@@ -89,7 +90,8 @@ int main(void)
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(S + G2),
- sizeof(char),(void *)S);
+ sizeof(char),(void *)S,
+ (void *)(& S));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(S + G2)",25);
__e_acsl_assert(*(S + G2) == 'o',(char *)"Assertion",(char *)"main",
@@ -111,7 +113,8 @@ int main(void)
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)S2,
sizeof(char),
- (void *)S2);
+ (void *)S2,
+ (void *)(& S2));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"Assertion",
(char *)"main",(char *)"\\valid_read(S2)",27);
}
@@ -126,7 +129,7 @@ int main(void)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)SS,sizeof(char),
- (void *)SS);
+ (void *)SS,(void *)(& SS));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
index 7fdd651b70f3028eb08a56e0610a46feeb0c5e47..9d38af490866b14548d15b6898cd2ef592d5d6b3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
@@ -13,7 +13,7 @@ int main(int argc, char **argv)
__e_acsl_store_block((void *)(& argv),(size_t)8);
__e_acsl_store_block((void *)(& argc),(size_t)4);
__gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int),
- (void *)(& argc));
+ (void *)(& argc),(void *)(& argc));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&argc)",10);
}
@@ -23,6 +23,7 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& argv),sizeof(char **),
+ (void *)(& argv),
(void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
(char *)"main",(char *)"\\valid(&argv)",11);
@@ -40,7 +41,8 @@ int main(int argc, char **argv)
{
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)(argv + __gen_e_acsl_k),
- sizeof(char *),(void *)argv);
+ sizeof(char *),(void *)argv,
+ (void *)(& argv));
if (__gen_e_acsl_valid_3) ;
else {
__gen_e_acsl_forall = 0;
@@ -82,7 +84,8 @@ int main(int argc, char **argv)
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(argv + argc),
sizeof(char *),
- (void *)argv);
+ (void *)argv,
+ (void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv + argc)",15);
/*@ assert Value: mem_access: \valid_read(argv + argc); */
@@ -102,14 +105,16 @@ int main(int argc, char **argv)
int __gen_e_acsl_valid_4;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(argv + argc),
sizeof(char *),
- (void *)argv);
+ (void *)argv,
+ (void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(argv + argc)",16);
/*@ assert Value: mem_access: \valid_read(argv + argc); */
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)*(argv + argc),
sizeof(char),
- (void *)*(argv + argc));
+ (void *)*(argv + argc),
+ (void *)(argv + argc));
__gen_e_acsl_and = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and = 0;
@@ -137,13 +142,15 @@ int main(int argc, char **argv)
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(
argv + i),
sizeof(char *),
- (void *)argv);
+ (void *)argv,
+ (void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(argv + i)",19);
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)*(argv + i),
sizeof(char),
- (void *)*(argv + i));
+ (void *)*(argv + i),
+ (void *)(argv + i));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_5;
}
else __gen_e_acsl_and_2 = 0;
@@ -166,14 +173,16 @@ int main(int argc, char **argv)
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(
argv + i),
sizeof(char *),
- (void *)argv);
+ (void *)argv,
+ (void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(argv + i)",
20);
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)(*(argv + i) + __gen_e_acsl_k_2),
sizeof(char),
- (void *)*(argv + i));
+ (void *)*(argv + i),
+ (void *)(argv + i));
if (__gen_e_acsl_valid_6) ;
else {
__gen_e_acsl_forall_2 = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
index 13346d3e1296f0ce49d1a2edc59733c155105fa6..016ac8c105dc2a9c44897bdeb88e6213353149c2 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
@@ -24,7 +24,8 @@ int main(int argc, char const **argv)
sizeof(char *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(char),(void *)p);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(char),(void *)p,
+ (void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
}
else __gen_e_acsl_and = 0;
@@ -61,7 +62,7 @@ int main(int argc, char const **argv)
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(char),
- (void *)p);
+ (void *)p,(void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and_2 = 0;
@@ -99,7 +100,7 @@ int main(int argc, char const **argv)
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)a,sizeof(char),
- (void *)a);
+ (void *)a,(void *)(& a));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_3 = 0;
@@ -137,7 +138,7 @@ int main(int argc, char const **argv)
if (__gen_e_acsl_initialized_4) {
int __gen_e_acsl_valid_4;
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)a,sizeof(char),
- (void *)a);
+ (void *)a,(void *)(& a));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
}
else __gen_e_acsl_and_4 = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
index feb03dbd2b4a2d8aa86b79edebe6756bd331fbc4..aa98ce917a78fe13add39ee46ff574cbfe170643 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
@@ -23,7 +23,8 @@ int main(void)
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,sizeof(int),
- (void *)p);
+ (void *)p,
+ (void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid_read;
}
else __gen_e_acsl_and = 0;
@@ -69,7 +70,8 @@ int main(void)
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& t[2] - i),
sizeof(int),
- (void *)(& t[2]));
+ (void *)(& t[2]),
+ (void *)(& t[2] - i));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(&t[2] - i)",19);
@@ -95,7 +97,8 @@ int main(void)
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)p,
sizeof(int),
- (void *)p);
+ (void *)p,
+ (void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_read_3;
}
else __gen_e_acsl_and_2 = 0;
@@ -111,7 +114,8 @@ int main(void)
{
int __gen_e_acsl_valid_read_4;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + k),
- sizeof(int),(void *)p);
+ sizeof(int),(void *)p,
+ (void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(p + k)",27);
__e_acsl_assert(*(p + k) == 3,(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
index bd5e5603a6b3a8005912528a5ac5944afe66c359..7a6427a80f305481e08342ba5f99edcac4e9e41b 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
@@ -22,7 +22,7 @@ int main(void)
{
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)stderr,sizeof(FILE),
- (void *)stderr);
+ (void *)stderr,(void *)(& stderr));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(__fc_stderr)",8);
}
@@ -32,7 +32,7 @@ int main(void)
{
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)stdin,sizeof(FILE),
- (void *)stdin);
+ (void *)stdin,(void *)(& stdin));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
(char *)"main",(char *)"\\valid(__fc_stdin)",9);
}
@@ -42,7 +42,8 @@ int main(void)
{
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)stdout,sizeof(FILE),
- (void *)stdout);
+ (void *)stdout,
+ (void *)(& stdout));
__e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Assertion",
(char *)"main",(char *)"\\valid(__fc_stdout)",10);
}
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index e691f509d86dee0d4759f8e8fe73bac53dd15422..2f191f1a35c64504ade1430e2855676f0f189a44 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -592,6 +592,11 @@ and mmodel_call_with_size ~loc kf name ctx env t =
and mmodel_call_valid ~loc kf name ctx env t =
let e, env = term_to_exp kf (Env.rte env true) t in
let base, _ = Misc.ptr_index ~loc e in
+ let base_addr = match base.enode with
+ | AddrOf _ -> e
+ | Lval(lv) | StartOf(lv) -> Cil.mkAddrOf ~loc lv
+ | _ -> assert false
+ in
let _, res, env =
Env.new_var
~loc
@@ -603,7 +608,7 @@ and mmodel_call_valid ~loc kf name ctx env t =
let ty = get_c_term_type t.term_type in
let sizeof = mk_ptr_sizeof ty loc in
let fname = Misc.mk_api_name name in
- let args = [ e; sizeof; base ] in
+ let args = [ e; sizeof; base; base_addr ] in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
in
res, env