diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index b68a16c8ae191100bf7696cdd39403fb8ce7fd16..977ef210fd92cc5c805231b45f0c8c4027f99924 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,8 @@
Plugin E-ACSL <next-release>
############################
+-* E-ACSL [2021-06-14] Fix pointer address on memory annotations with
+ range indices (frama-c/e-acsl#148).
-* E-ACSL [2021-06-04] Do not translate contracts of E-ACSL built-ins.
#############################
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 41fedc2159be7bf64f11fbd1c3ae434ab874fb70..8c05dec02008ff757e793a7f2ae32a355f3dae04 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -339,7 +339,6 @@ let extract_quantifiers ~loc args =
([], [])
args
-
(* [call_with_tset
~loc
~arg_from_range
@@ -443,7 +442,7 @@ let call_with_tset ~loc ~arg_from_range ~arg_from_term ?(prepend_n_args=false) k
assert (Logic_const.is_set_type t.term_type);
let lty_noset = Logic_const.type_of_element t.term_type in
let ptr =
- Logic_const.taddrof ~loc (TVar lv, TNoOffset) lty_noset
+ Logic_const.term ~loc (TStartOf (TVar lv, TNoOffset)) lty_noset
in
arg_from_range ~loc kf env rev_args ptr r p
| _ ->
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 2c4ace3aea337c3113b74e6f977b64824b33b8b9..562aa9e561d6017fbaa23d3676b9aec6b783a5b9 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -868,9 +868,11 @@ and predicate_content_to_exp ?name kf env p =
call_valid t p
end else begin
match t.term_node, t.term_type with
- | TLval tlv, Ctype ty ->
+ | TLval tlv, lty ->
let init =
- Logic_const.pinitialized ~loc (llabel, Misc.term_addr_of ~loc tlv ty)
+ Logic_const.pinitialized
+ ~loc
+ (llabel, Logic_utils.mk_logic_AddrOf ~loc tlv lty)
in
Typing.type_named_predicate ~must_clear:false init;
let p = Logic_const.pand ~loc (init, p) in
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 95e8177eaab3ea44db06987a7c26de20c2d803c7..69a788246b64b72045d19274ffa853a55c0385e5 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -77,9 +77,6 @@ let rec add_casts tys e =
let e = Cil.mkCast ~newt e in
add_casts tl e
-let term_addr_of ~loc tlv ty =
- Logic_const.taddrof ~loc tlv (Ctype (TPtr(ty, [])))
-
let cty = function
| Ctype ty -> ty
| lty -> Options.fatal "Expecting a C type. Got %a" Printer.pp_logic_type lty
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 60c4934e4951628512da4010fb60a44787d60560..daddb3fee0821e40d2420494dd0254f1d8f40e66 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -44,8 +44,6 @@ val is_fc_stdlib_generated: varinfo -> bool
(** Returns true if the [varinfo] is a generated stdlib function. (For instance
generated function by the Variadic plug-in. *)
-val term_addr_of: loc:location -> term_lval -> typ -> term
-
val cty: logic_type -> typ
(** Assume that the logic type is indeed a C type. Just return it. *)
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;
}