diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
index 51086e0b41d908642c41ed0b46ae6f42dcfdc886..7aefc7c01edd90fdfc8d85a440001a077bc02a38 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
@@ -49,9 +49,9 @@ int main(void)
__gen_e_acsl_size_2 = 1 * ((9 - 0) + 1);
if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& t + 1 * 0),
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(t + 1 * 0),
(size_t)__gen_e_acsl_if_2,
- (void *)(& t),(void *)0);
+ (void *)(t),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_2,1,"Assertion","main",
"\\valid(&t[0 .. 9])","tests/bts/bts2406.c",11);
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
index 94379691eab1ea1d71c19fad33b4355b9b084f52..75af517de674f5cbbd46334051db14ab629e1f01 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
@@ -139,9 +139,9 @@ int main(void)
__gen_e_acsl_size_6 = 8 * ((2 - 0) + 1);
if (__gen_e_acsl_size_6 <= 0) __gen_e_acsl_if_6 = 0;
else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
- __gen_e_acsl_valid_6 = __e_acsl_valid((void *)((char *)(& t) + 8 * 0),
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)((char *)(t) + 8 * 0),
(size_t)__gen_e_acsl_if_6,
- (void *)(& t),(void *)0);
+ (void *)(t),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_6,1,"Assertion","main",
"\\valid(&t[0 .. 2])",
"tests/memory/ranges_in_builtins.c",31);
@@ -154,9 +154,9 @@ int main(void)
__gen_e_acsl_size_7 = 8 * ((5 - 3) + 1);
if (__gen_e_acsl_size_7 <= 0) __gen_e_acsl_if_7 = 0;
else __gen_e_acsl_if_7 = __gen_e_acsl_size_7;
- __gen_e_acsl_valid_7 = __e_acsl_valid((void *)((char *)(& t) + 8 * 3),
+ __gen_e_acsl_valid_7 = __e_acsl_valid((void *)((char *)(t) + 8 * 3),
(size_t)__gen_e_acsl_if_7,
- (void *)(& t),(void *)0);
+ (void *)(t),(void *)0);
__e_acsl_assert(! __gen_e_acsl_valid_7,1,"Assertion","main",
"!\\valid(&t[3 .. 5])",
"tests/memory/ranges_in_builtins.c",32);
@@ -174,7 +174,7 @@ int main(void)
__gen_e_acsl_size_8 = 8 * ((1 - 0) + 1);
if (__gen_e_acsl_size_8 <= 0) __gen_e_acsl_if_8 = 0;
else __gen_e_acsl_if_8 = __gen_e_acsl_size_8;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)(& t2) +
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)(t2) +
8 * 0),
(size_t)__gen_e_acsl_if_8);
__e_acsl_assert(__gen_e_acsl_initialized,1,"Assertion","main",
@@ -189,7 +189,7 @@ int main(void)
__gen_e_acsl_size_9 = 8 * ((3 - 2) + 1);
if (__gen_e_acsl_size_9 <= 0) __gen_e_acsl_if_9 = 0;
else __gen_e_acsl_if_9 = __gen_e_acsl_size_9;
- __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)((char *)(& t2) +
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)((char *)(t2) +
8 * 2),
(size_t)__gen_e_acsl_if_9);
__e_acsl_assert(! __gen_e_acsl_initialized_2,1,"Assertion","main",
@@ -409,7 +409,26 @@ int main(void)
__e_acsl_store_block((void *)(& c),(size_t)1);
__e_acsl_full_init((void *)(& c));
__gen_e_acsl_f(& c,(long)5);
+ char t5[4] = {(char)'a', (char)'b', (char)'c', (char)'d'};
+ __e_acsl_store_block((void *)(t5),(size_t)4);
+ __e_acsl_full_init((void *)(& t5));
+ {
+ int __gen_e_acsl_size_15;
+ int __gen_e_acsl_if_15;
+ int __gen_e_acsl_valid_10;
+ __gen_e_acsl_size_15 = 1 * ((3 - 2) + 1);
+ if (__gen_e_acsl_size_15 <= 0) __gen_e_acsl_if_15 = 0;
+ else __gen_e_acsl_if_15 = __gen_e_acsl_size_15;
+ __gen_e_acsl_valid_10 = __e_acsl_valid((void *)(t5 + 1 * 2),
+ (size_t)__gen_e_acsl_if_15,
+ (void *)(t5),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_10,1,"Assertion","main",
+ "\\valid(&t5[2 .. 3])",
+ "tests/memory/ranges_in_builtins.c",78);
+ }
+ /*@ assert \valid(&t5[2 .. 3]); */ ;
__retres = 0;
+ __e_acsl_delete_block((void *)(t5));
__e_acsl_delete_block((void *)(& c));
__e_acsl_delete_block((void *)(& multi_dynamic));
__e_acsl_delete_block((void *)(& s));
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c
index b18704e155e475945183c454da4959126c744fbd..d5781612a5d4924d950f9d56137aeab3740f6e8e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c
@@ -138,10 +138,10 @@ int main(void)
__gen_e_acsl_size = 8 * ((9 - 0) + 1);
if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
else __gen_e_acsl_if = __gen_e_acsl_size;
- __gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 0),
(size_t)__gen_e_acsl_if,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 9]); */
__e_acsl_assert(__gen_e_acsl_valid_read_8,1,"RTE","main",
@@ -150,10 +150,10 @@ int main(void)
__gen_e_acsl_size_2 = 8 * ((19 - 10) + 1);
if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
- __gen_e_acsl_valid_read_9 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_9 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 10),
(size_t)__gen_e_acsl_if_2,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[10 .. 19]); */
__e_acsl_assert(__gen_e_acsl_valid_read_9,1,"RTE","main",
@@ -166,10 +166,10 @@ int main(void)
if (__gen_e_acsl_size_4 <= 0) __gen_e_acsl_if_4 = 0;
else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
__gen_e_acsl_separated_3 = __e_acsl_separated((size_t)2,
- (char *)(& array) + 8 * 0,
+ (char *)(array) + 8 * 0,
__gen_e_acsl_if_3,
- (char *)(& array) +
- 8 * 10,__gen_e_acsl_if_4);
+ (char *)(array) + 8 * 10,
+ __gen_e_acsl_if_4);
__e_acsl_assert(__gen_e_acsl_separated_3,1,"Assertion","main",
"\\separated(&array[0 .. 9], &array[10 .. 19])",
"tests/memory/separated.c",21);
@@ -190,10 +190,10 @@ int main(void)
__gen_e_acsl_size_5 = 8 * ((10 - 0) + 1);
if (__gen_e_acsl_size_5 <= 0) __gen_e_acsl_if_5 = 0;
else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
- __gen_e_acsl_valid_read_10 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_10 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 0),
(size_t)__gen_e_acsl_if_5,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 10]); */
__e_acsl_assert(__gen_e_acsl_valid_read_10,1,"RTE","main",
@@ -202,10 +202,10 @@ int main(void)
__gen_e_acsl_size_6 = 8 * ((15 - 5) + 1);
if (__gen_e_acsl_size_6 <= 0) __gen_e_acsl_if_6 = 0;
else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
- __gen_e_acsl_valid_read_11 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_11 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 5),
(size_t)__gen_e_acsl_if_6,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[5 .. 15]); */
__e_acsl_assert(__gen_e_acsl_valid_read_11,1,"RTE","main",
@@ -218,9 +218,9 @@ int main(void)
if (__gen_e_acsl_size_8 <= 0) __gen_e_acsl_if_8 = 0;
else __gen_e_acsl_if_8 = __gen_e_acsl_size_8;
__gen_e_acsl_separated_4 = __e_acsl_separated((size_t)2,
- (char *)(& array) + 8 * 0,
+ (char *)(array) + 8 * 0,
__gen_e_acsl_if_7,
- (char *)(& array) + 8 * 5,
+ (char *)(array) + 8 * 5,
__gen_e_acsl_if_8);
__e_acsl_assert(! __gen_e_acsl_separated_4,1,"Assertion","main",
"!\\separated(&array[0 .. 10], &array[5 .. 15])",
@@ -242,10 +242,10 @@ int main(void)
__gen_e_acsl_size_9 = 8 * ((19 - 0) + 1);
if (__gen_e_acsl_size_9 <= 0) __gen_e_acsl_if_9 = 0;
else __gen_e_acsl_if_9 = __gen_e_acsl_size_9;
- __gen_e_acsl_valid_read_12 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_12 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 0),
(size_t)__gen_e_acsl_if_9,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 19]); */
__e_acsl_assert(__gen_e_acsl_valid_read_12,1,"RTE","main",
@@ -254,10 +254,10 @@ int main(void)
__gen_e_acsl_size_10 = 8 * ((15 - 5) + 1);
if (__gen_e_acsl_size_10 <= 0) __gen_e_acsl_if_10 = 0;
else __gen_e_acsl_if_10 = __gen_e_acsl_size_10;
- __gen_e_acsl_valid_read_13 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_13 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 5),
(size_t)__gen_e_acsl_if_10,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[5 .. 15]); */
__e_acsl_assert(__gen_e_acsl_valid_read_13,1,"RTE","main",
@@ -270,9 +270,9 @@ int main(void)
if (__gen_e_acsl_size_12 <= 0) __gen_e_acsl_if_12 = 0;
else __gen_e_acsl_if_12 = __gen_e_acsl_size_12;
__gen_e_acsl_separated_5 = __e_acsl_separated((size_t)2,
- (char *)(& array) + 8 * 0,
+ (char *)(array) + 8 * 0,
__gen_e_acsl_if_11,
- (char *)(& array) + 8 * 5,
+ (char *)(array) + 8 * 5,
__gen_e_acsl_if_12);
__e_acsl_assert(! __gen_e_acsl_separated_5,1,"Assertion","main",
"!\\separated(&array[0 .. 19], &array[5 .. 15])",
@@ -323,10 +323,10 @@ int main(void)
__gen_e_acsl_size_13 = 8 * ((1 - 0) + 1);
if (__gen_e_acsl_size_13 <= 0) __gen_e_acsl_if_13 = 0;
else __gen_e_acsl_if_13 = __gen_e_acsl_size_13;
- __gen_e_acsl_valid_read_16 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_16 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 0),
(size_t)__gen_e_acsl_if_13,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 1]); */
__e_acsl_assert(__gen_e_acsl_valid_read_16,1,"RTE","main",
@@ -335,10 +335,10 @@ int main(void)
__gen_e_acsl_size_14 = 8 * ((2 - 1) + 1);
if (__gen_e_acsl_size_14 <= 0) __gen_e_acsl_if_14 = 0;
else __gen_e_acsl_if_14 = __gen_e_acsl_size_14;
- __gen_e_acsl_valid_read_17 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_17 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 1),
(size_t)__gen_e_acsl_if_14,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[1 .. 2]); */
__e_acsl_assert(__gen_e_acsl_valid_read_17,1,"RTE","main",
@@ -351,9 +351,9 @@ int main(void)
if (__gen_e_acsl_size_16 <= 0) __gen_e_acsl_if_16 = 0;
else __gen_e_acsl_if_16 = __gen_e_acsl_size_16;
__gen_e_acsl_separated_7 = __e_acsl_separated((size_t)2,
- (char *)(& array) + 8 * 0,
+ (char *)(array) + 8 * 0,
__gen_e_acsl_if_15,
- (char *)(& array) + 8 * 1,
+ (char *)(array) + 8 * 1,
__gen_e_acsl_if_16);
__e_acsl_assert(! __gen_e_acsl_separated_7,1,"Assertion","main",
"!\\separated(&array[0 .. 1], &array[1 .. 2])",
@@ -375,10 +375,10 @@ int main(void)
__gen_e_acsl_size_17 = 8 * ((5 - 15) + 1);
if (__gen_e_acsl_size_17 <= 0) __gen_e_acsl_if_17 = 0;
else __gen_e_acsl_if_17 = __gen_e_acsl_size_17;
- __gen_e_acsl_valid_read_18 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_18 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 15),
(size_t)__gen_e_acsl_if_17,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[15 .. 5]); */
__e_acsl_assert(__gen_e_acsl_valid_read_18,1,"RTE","main",
@@ -387,10 +387,10 @@ int main(void)
__gen_e_acsl_size_18 = 8 * ((19 - 0) + 1);
if (__gen_e_acsl_size_18 <= 0) __gen_e_acsl_if_18 = 0;
else __gen_e_acsl_if_18 = __gen_e_acsl_size_18;
- __gen_e_acsl_valid_read_19 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_19 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 0),
(size_t)__gen_e_acsl_if_18,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 19]); */
__e_acsl_assert(__gen_e_acsl_valid_read_19,1,"RTE","main",
@@ -403,10 +403,9 @@ int main(void)
if (__gen_e_acsl_size_20 <= 0) __gen_e_acsl_if_20 = 0;
else __gen_e_acsl_if_20 = __gen_e_acsl_size_20;
__gen_e_acsl_separated_8 = __e_acsl_separated((size_t)2,
- (char *)(& array) +
- 8 * 15,
+ (char *)(array) + 8 * 15,
__gen_e_acsl_if_19,
- (char *)(& array) + 8 * 0,
+ (char *)(array) + 8 * 0,
__gen_e_acsl_if_20);
__e_acsl_assert(__gen_e_acsl_separated_8,1,"Assertion","main",
"\\separated(&array[15 .. 5], &array[0 .. 19])",
@@ -428,10 +427,10 @@ int main(void)
__gen_e_acsl_size_21 = 8 * ((-3 - 0) + 1);
if (__gen_e_acsl_size_21 <= 0) __gen_e_acsl_if_21 = 0;
else __gen_e_acsl_if_21 = __gen_e_acsl_size_21;
- __gen_e_acsl_valid_read_20 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_20 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 0),
(size_t)__gen_e_acsl_if_21,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. -3]); */
__e_acsl_assert(__gen_e_acsl_valid_read_20,1,"RTE","main",
@@ -440,10 +439,10 @@ int main(void)
__gen_e_acsl_size_22 = 8 * ((19 - 0) + 1);
if (__gen_e_acsl_size_22 <= 0) __gen_e_acsl_if_22 = 0;
else __gen_e_acsl_if_22 = __gen_e_acsl_size_22;
- __gen_e_acsl_valid_read_21 = __e_acsl_valid_read((void *)((char *)(& array) +
+ __gen_e_acsl_valid_read_21 = __e_acsl_valid_read((void *)((char *)(array) +
8 * 0),
(size_t)__gen_e_acsl_if_22,
- (void *)(& array),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 19]); */
__e_acsl_assert(__gen_e_acsl_valid_read_21,1,"RTE","main",
@@ -456,9 +455,9 @@ int main(void)
if (__gen_e_acsl_size_24 <= 0) __gen_e_acsl_if_24 = 0;
else __gen_e_acsl_if_24 = __gen_e_acsl_size_24;
__gen_e_acsl_separated_9 = __e_acsl_separated((size_t)2,
- (char *)(& array) + 8 * 0,
+ (char *)(array) + 8 * 0,
__gen_e_acsl_if_23,
- (char *)(& array) + 8 * 0,
+ (char *)(array) + 8 * 0,
__gen_e_acsl_if_24);
__e_acsl_assert(__gen_e_acsl_separated_9,1,"Assertion","main",
"\\separated(&array[0 .. -3], &array[0 .. 19])",
diff --git a/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
index 7af22946ecf5b94fc25c67c1ef326e157878a2ef..0ffeae418fc697664a9e93b151c5536cf3343d57 100644
--- a/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
@@ -73,4 +73,9 @@ int main(void) {
char c = 'w';
f(&c, 5);
+
+ char t5[4] = {'a', 'b', 'c', 'd'};
+ /*@ assert \valid(&t5[2..3]); */
+
+ return 0;
}