diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 05e7510ee516f4b4dbf613b0ecd8594eebd852bf..1ef3673d4e0349d506407602f7ae5da12c76a8b9 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-03-25] Fix wrong computation of the base pointer when
+ calling \valid predicate leading to undetected array overflows.
-* E-ACSL [2021-02-24] Fix crash when running another analysis after
E-ACSL caused by E-ACSL breaking some internal kernel invariant
(frama-c/e-acsl#145).
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 524df6755b2c5334a2db69a67b89e771eda1e1c3..976c5c91d3ea809a1739bb30fd0b722f0f1b70d3 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -507,12 +507,12 @@ let call_valid ~loc kf name ctx env t p =
assert (name = "valid" || name = "valid_read");
let arg_from_term ~loc kf env rev_args t _p =
let ptr, size, env = term_to_ptr_and_size ~loc kf env t in
- let base, base_addr = Misc.ptr_base ~loc ptr in
+ let base, base_addr = Misc.ptr_base_and_base_addr ~loc ptr in
base_addr :: base :: size :: ptr :: rev_args, env
in
let arg_from_range ~loc kf env rev_args ptr r p =
let ptr, size, env = range_to_ptr_and_size ~loc kf env ptr r p in
- let base, base_addr = Misc.ptr_base ~loc ptr in
+ let base, base_addr = Misc.ptr_base_and_base_addr ~loc ptr in
base_addr :: base :: size :: ptr :: rev_args, env
in
let prepend_n_args = false in
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index a1c0843ccde0dc359b576ead5198b074e2dc31f0..919780e867c88c0734ec8a500bbc55b7c3ab6683 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -146,9 +146,9 @@ let assign ?(ltype) lhs rhs loc =
in
match Cil.unrollType ltype with
| TPtr _ ->
- let base, _ = Misc.ptr_index rhs in
+ let base = Misc.ptr_base ~loc:rhs.eloc rhs in
let rhs, flow =
- (match base.enode with
+ (match (Cil.stripCasts base).enode with
| AddrOf _
| StartOf _ -> rhs, Direct
(* Unary operator describes !, ~ or -: treat it same as Const since
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 11c177a27354c2c1881b88aece05394544979fff..92d0e9bfef74a16e235e04f84301a1f25b2ce6cc 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -21,7 +21,6 @@
(**************************************************************************)
open Cil_types
-open Cil_datatype
(* ************************************************************************** *)
(** {2 Handling the E-ACSL's C-libraries, part I} *)
@@ -60,6 +59,21 @@ let result_vi kf = match result_lhost kf with
(** {2 Other stuff} *)
(* ************************************************************************** *)
+let strip_casts e =
+ let rec aux casts e =
+ match e.enode with
+ | CastE(ty, e') -> aux (ty :: casts) e'
+ | _ -> e, casts
+ in
+ aux [] e
+
+let rec add_casts tys e =
+ match tys with
+ | [] -> e
+ | newt :: tl ->
+ 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, [])))
@@ -67,36 +81,52 @@ let cty = function
| Ctype ty -> ty
| lty -> Options.fatal "Expecting a C type. Got %a" Printer.pp_logic_type lty
-let rec ptr_index ?(loc=Location.unknown) ?(index=(Cil.zero loc)) exp =
- let arith_op = function
- | MinusPI -> MinusA
- | PlusPI -> PlusA
- | IndexPI -> PlusA
- | _ -> assert false in
+(* Replace all trailing array subscripts of an lval with zero indices. *)
+let rec shift_offsets lv loc =
+ let lv, off = Cil.removeOffsetLval lv in
+ match off with
+ | Index _ ->
+ let lv = shift_offsets lv loc in
+ (* since the offset has been removed at the start of the function, add a new
+ 0 offset to preserve the type of the lvalue. *)
+ Cil.addOffsetLval (Index (Cil.zero ~loc, NoOffset)) lv
+ | NoOffset | Field _ -> Cil.addOffsetLval off lv
+
+let rec ptr_base ~loc exp =
match exp.enode with
- | BinOp(op, lhs, rhs, _) ->
+ | BinOp(op, lhs, _, _) ->
(match op with
(* Pointer arithmetic: split pointer and integer parts *)
- | MinusPI | PlusPI | IndexPI ->
- let index = Cil.mkBinOp exp.eloc (arith_op op) index rhs in
- ptr_index ~index lhs
+ | MinusPI | PlusPI | IndexPI -> ptr_base ~loc lhs
(* Other arithmetic: treat the whole expression as pointer address *)
| MinusPP | PlusA | MinusA | Mult | Div | Mod
| BAnd | BXor | BOr | Shiftlt | Shiftrt
- | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr -> (exp, index))
- | CastE _ -> ptr_index ~loc ~index (Cil.stripCasts exp)
- | Info (exp, _) -> ptr_index ~loc ~index exp
- | Const _ | StartOf _ | AddrOf _ | Lval _ | UnOp _ -> (exp, index)
+ | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr -> exp)
+ (* AddressOf: if it is an addressof array then replace all trailing offsets
+ with zero offsets to get the base. *)
+ | AddrOf lv -> Cil.mkAddrOf ~loc (shift_offsets lv loc)
+ (* StartOf already points to the start of an array, return exp directly *)
+ | StartOf _ -> exp
+ (* Cast: strip cast and continue, then recast to original type. *)
+ | CastE _ ->
+ let exp, casts = strip_casts exp in
+ let base = ptr_base ~loc exp in
+ add_casts casts base
+ | Info (exp, _) -> ptr_base ~loc exp
+ | Const _ | Lval _ | UnOp _ -> exp
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
-> assert false
-let ptr_base ~loc e =
- let base, _ = ptr_index ~loc e in
- let base_addr = match base.enode with
- | AddrOf _ | Const _ -> Cil.zero ~loc
- | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
+let ptr_base_and_base_addr ~loc e =
+ let rec ptr_base_addr ~loc base =
+ match base.enode with
+ | AddrOf _ | StartOf _ | Const _ -> Cil.zero ~loc
+ | Lval lv -> Cil.mkAddrOrStartOf ~loc lv
+ | CastE _ -> ptr_base_addr ~loc (Cil.stripCasts base)
| _ -> assert false
in
+ let base = ptr_base ~loc e in
+ let base_addr = ptr_base_addr ~loc base in
base, base_addr
(* TODO: should not be in this file *)
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index f5a2c28359790d6d6cd4a9285b30c3333944bebe..60c4934e4951628512da4010fb60a44787d60560 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -49,12 +49,11 @@ 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. *)
-val ptr_index: ?loc:location -> ?index:exp -> exp
- -> Cil_types.exp * Cil_types.exp
-(** Split pointer-arithmetic expression of the type [p + i] into its
- pointer and integer parts. *)
+val ptr_base: loc:location -> exp -> exp
+(** Takes an expression [e] and return [base] where [base] is the address [p]
+ if [e] is of the form [p + i] and [e] otherwise. *)
-val ptr_base: loc:location -> exp -> exp * exp
+val ptr_base_and_base_addr: loc:location -> exp -> exp * exp
(* Takes an expression [e] and return a tuple [(base, base_addr)] where [base]
is the address [p] if [e] is of the form [p + i] and [e] otherwise, and
[base_addr] is the address [&p] if [e] is of the form [p + i] and 0
@@ -94,6 +93,17 @@ val extract_uncoerced_lval: exp -> exp option
If at some point the expression is neither a [CastE] nor an [Lval], then
return [None]. *)
+val strip_casts: exp -> exp * typ list
+(** [strip casts e] strips the casts from the expression [e] and returns the
+ uncasted expression and the list of casts that were removed in order of
+ application. For example calling [strip_casts ((A)((B)((C)e)))] will return
+ the expression [e] and the list [[C; B; A]]. *)
+
+val add_casts: typ list -> exp -> exp
+(** [add_casts typs e] successively adds the casts in [typs] to the expression
+ [e]. For example calling [add_casts [C; B; A] e] will return the expression
+ [(A)((B)((C)e))]. *)
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
index 73ea4bf5ab15bfb8cdebf3895769ca0f0947ec9d..0507dfdf3bd3138baa62a3d7e65542f80bfb6144 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
@@ -104,7 +104,7 @@ void arrays(void)
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& (*((int (*)[3])g))[__gen_e_acsl_iter_4]),
sizeof(int),
- (void *)(& (*((int (*)[3])g))[__gen_e_acsl_iter_4]),
+ (void *)(*((int (*)[3])g)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[3])g))[__gen_e_acsl_iter_4])",
@@ -132,7 +132,7 @@ void arrays(void)
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(*((int (*)[])g)),
sizeof(int),
(void *)(*((int (*)[])g)),
- (void *)(*((int (*)[])g)));
+ (void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","arrays",
"mem_access: \\valid_read((int *)*((int (*)[])g))",
"tests/arith/array.i",41);
@@ -147,7 +147,7 @@ void arrays(void)
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*((int (*)[])g))[__gen_e_acsl_iter_5]),
sizeof(int),
- (void *)(& (*((int (*)[])g))[__gen_e_acsl_iter_5]),
+ (void *)(*((int (*)[])g)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[])g))[__gen_e_acsl_iter_5])",
@@ -176,7 +176,7 @@ void arrays(void)
int __gen_e_acsl_valid_read_4;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*((int (*)[3])f))[__gen_e_acsl_iter_6]),
sizeof(int),
- (void *)(& (*((int (*)[3])f))[__gen_e_acsl_iter_6]),
+ (void *)(*((int (*)[3])f)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_4,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[3])f))[__gen_e_acsl_iter_6])",
@@ -204,7 +204,7 @@ void arrays(void)
__gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(*((int (*)[])f)),
sizeof(int),
(void *)(*((int (*)[])f)),
- (void *)(*((int (*)[])f)));
+ (void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_5,"RTE","arrays",
"mem_access: \\valid_read((int *)*((int (*)[])f))",
"tests/arith/array.i",43);
@@ -219,7 +219,7 @@ void arrays(void)
int __gen_e_acsl_valid_read_6;
__gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)(& (*((int (*)[])f))[__gen_e_acsl_iter_7]),
sizeof(int),
- (void *)(& (*((int (*)[])f))[__gen_e_acsl_iter_7]),
+ (void *)(*((int (*)[])f)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_6,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[])f))[__gen_e_acsl_iter_7])",
@@ -324,14 +324,14 @@ void arrays(void)
int __gen_e_acsl_valid_read_8;
__gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(& (*((int (*)[3])l))[__gen_e_acsl_iter_11]),
sizeof(int),
- (void *)(& (*((int (*)[3])l))[__gen_e_acsl_iter_11]),
+ (void *)(*((int (*)[3])l)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_7,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[3])l))[__gen_e_acsl_iter_11])",
"tests/arith/array.i",55);
__gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)(& (*((int (*)[3])m))[__gen_e_acsl_iter_11]),
sizeof(int),
- (void *)(& (*((int (*)[3])m))[__gen_e_acsl_iter_11]),
+ (void *)(*((int (*)[3])m)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_8,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[3])m))[__gen_e_acsl_iter_11])",
@@ -362,14 +362,14 @@ void arrays(void)
int __gen_e_acsl_valid_read_10;
__gen_e_acsl_valid_read_9 = __e_acsl_valid_read((void *)(& (*((int (*)[3])l))[__gen_e_acsl_iter_12]),
sizeof(int),
- (void *)(& (*((int (*)[3])l))[__gen_e_acsl_iter_12]),
+ (void *)(*((int (*)[3])l)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_9,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[3])l))[__gen_e_acsl_iter_12])",
"tests/arith/array.i",56);
__gen_e_acsl_valid_read_10 = __e_acsl_valid_read((void *)(& (*((int (*)[3])n))[__gen_e_acsl_iter_12]),
sizeof(int),
- (void *)(& (*((int (*)[3])n))[__gen_e_acsl_iter_12]),
+ (void *)(*((int (*)[3])n)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_10,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[3])n))[__gen_e_acsl_iter_12])",
@@ -446,14 +446,14 @@ void arrays(void)
int __gen_e_acsl_valid_read_12;
__gen_e_acsl_valid_read_11 = __e_acsl_valid_read((void *)(& (*((int (*)[2])l))[__gen_e_acsl_iter_15]),
sizeof(int),
- (void *)(& (*((int (*)[2])l))[__gen_e_acsl_iter_15]),
+ (void *)(*((int (*)[2])l)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_11,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[2])l))[__gen_e_acsl_iter_15])",
"tests/arith/array.i",61);
__gen_e_acsl_valid_read_12 = __e_acsl_valid_read((void *)(& (*((int (*)[2])m))[__gen_e_acsl_iter_15]),
sizeof(int),
- (void *)(& (*((int (*)[2])m))[__gen_e_acsl_iter_15]),
+ (void *)(*((int (*)[2])m)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_12,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[2])m))[__gen_e_acsl_iter_15])",
@@ -484,14 +484,14 @@ void arrays(void)
int __gen_e_acsl_valid_read_14;
__gen_e_acsl_valid_read_13 = __e_acsl_valid_read((void *)(& (*((int (*)[2])l))[__gen_e_acsl_iter_16]),
sizeof(int),
- (void *)(& (*((int (*)[2])l))[__gen_e_acsl_iter_16]),
+ (void *)(*((int (*)[2])l)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_13,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[2])l))[__gen_e_acsl_iter_16])",
"tests/arith/array.i",62);
__gen_e_acsl_valid_read_14 = __e_acsl_valid_read((void *)(& (*((int (*)[2])n))[__gen_e_acsl_iter_16]),
sizeof(int),
- (void *)(& (*((int (*)[2])n))[__gen_e_acsl_iter_16]),
+ (void *)(*((int (*)[2])n)),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_14,"RTE","arrays",
"mem_access: \\valid_read(&(*((int (*)[2])n))[__gen_e_acsl_iter_16])",
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c
index e13edd15d57a19cfe1693bf1d92e7f6f5d0ec0a2..e1eb10cf0b34fa489941d19657abaaf775636270 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c
@@ -189,8 +189,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]),
+ sizeof(int),(void *)(buf),
(void *)0);
if (__gen_e_acsl_valid) ;
else {
@@ -216,8 +215,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]),
+ sizeof(int),(void *)(buf),
(void *)0);
if (__gen_e_acsl_valid_2) ;
else {
@@ -243,8 +241,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]),
+ sizeof(int),(void *)(buf),
(void *)0);
if (__gen_e_acsl_valid_3) ;
else {
@@ -287,8 +284,7 @@ int main(void)
int __gen_e_acsl_valid_4;
__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]),
+ sizeof(int),(void *)(buf),
(void *)0);
if (__gen_e_acsl_valid_4) ;
else {
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c
index ed0e31eeef3722d85e285e8dea7b1d52f8c2b71a..e77d7ee799b3a0b98732b30b6afed30c0fd84080 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c
@@ -77,14 +77,14 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__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 *)0);
__e_acsl_assert(__gen_e_acsl_valid_read,"RTE",
"atp_NORMAL_computeAverageAccel",
"mem_access: \\valid_read((int *)*__gen_e_acsl_at_6)",
"tests/bts/bts1326.i",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),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE",
"atp_NORMAL_computeAverageAccel",
@@ -92,7 +92,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
"tests/bts/bts1326.i",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),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE",
"atp_NORMAL_computeAverageAccel",
@@ -100,7 +100,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
"tests/bts/bts1326.i",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),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_4,"RTE",
"atp_NORMAL_computeAverageAccel",
@@ -108,7 +108,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
"tests/bts/bts1326.i",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),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_5,"RTE",
"atp_NORMAL_computeAverageAccel",
diff --git a/src/plugins/e-acsl/tests/memory/array_overflow.c b/src/plugins/e-acsl/tests/memory/array_overflow.c
new file mode 100644
index 0000000000000000000000000000000000000000..d002e455f4975a75dc9f7a58d8bdf28f1268796b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/array_overflow.c
@@ -0,0 +1,46 @@
+/* run.config_ci, run.config_dev
+ COMMENT: Array overflow
+*/
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <stddef.h>
+
+struct dat {
+ int arr[4];
+};
+
+struct dat2 {
+ struct dat *p[2];
+};
+
+struct dat3 {
+ int * arr;
+};
+
+void init4(int * arr, int start) {
+ for (int i = 0 ; i < 4 ; ++i) {
+ arr[i] = start + i;
+ }
+}
+
+int main() {
+ int a[4] = { 1, 2, 3, 4 };
+ int b[4] = { 5, 6, 7, 8 };
+
+ /*@ assert ! \valid(&a[4]); */
+
+ int * ap = a;
+ int * bp = b;
+
+ /*@ assert ! \valid(&((int[])ap)[4]); */
+
+ struct dat d = { .arr = { 4, 5, 6, 7 } };
+ struct dat dd = { .arr = { 1, 2, 3, 9 } };
+ struct dat2 d2 = { .p = { &d, &dd } };
+
+ /*@ assert ! \valid(&d.arr[4]); */
+ /*@ assert \valid(&d2.p[1]->arr[2]); */
+
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/array_overflow.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/array_overflow.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/array_overflow.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_array_overflow.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_array_overflow.c
new file mode 100644
index 0000000000000000000000000000000000000000..c2986d659a7059ffa15b8afb37a170807a1d8416
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_array_overflow.c
@@ -0,0 +1,90 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+#include "stdlib.h"
+struct dat {
+ int arr[4] ;
+};
+struct dat2 {
+ struct dat *p[2] ;
+};
+void init4(int *arr, int start)
+{
+ int i = 0;
+ while (i < 4) {
+ *(arr + i) = start + i;
+ i ++;
+ }
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ int a[4] = {1, 2, 3, 4};
+ __e_acsl_store_block((void *)(a),(size_t)16);
+ __e_acsl_full_init((void *)(& a));
+ int b[4] = {5, 6, 7, 8};
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& a[4]),sizeof(int),
+ (void *)(a),(void *)0);
+ __e_acsl_assert(! __gen_e_acsl_valid,"Assertion","main",
+ "!\\valid(&a[4])","tests/memory/array_overflow.c",31);
+ }
+ /*@ assert ¬\valid(&a[4]); */ ;
+ int *ap = a;
+ __e_acsl_store_block((void *)(& ap),(size_t)8);
+ __e_acsl_full_init((void *)(& ap));
+ int *bp = b;
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& (*((int (*)[])ap))[4]),
+ sizeof(int),
+ (void *)(*((int (*)[])ap)),
+ (void *)0);
+ __e_acsl_assert(! __gen_e_acsl_valid_2,"Assertion","main",
+ "!\\valid(&(*((int (*)[])ap))[4])",
+ "tests/memory/array_overflow.c",36);
+ }
+ /*@ assert ¬\valid(&(*((int (*)[])ap))[4]); */ ;
+ struct dat d = {.arr = {4, 5, 6, 7}};
+ __e_acsl_store_block((void *)(& d),(size_t)16);
+ __e_acsl_full_init((void *)(& d));
+ struct dat dd = {.arr = {1, 2, 3, 9}};
+ __e_acsl_store_block((void *)(& dd),(size_t)16);
+ __e_acsl_full_init((void *)(& dd));
+ struct dat2 d2 = {.p = {& d, & dd}};
+ __e_acsl_store_block((void *)(& d2),(size_t)16);
+ __e_acsl_full_init((void *)(& d2));
+ {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& d.arr[4]),sizeof(int),
+ (void *)(& d.arr[0]),(void *)0);
+ __e_acsl_assert(! __gen_e_acsl_valid_3,"Assertion","main",
+ "!\\valid(&d.arr[4])","tests/memory/array_overflow.c",42);
+ }
+ /*@ assert ¬\valid(&d.arr[4]); */ ;
+ {
+ int __gen_e_acsl_valid_4;
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& (d2.p[1])->arr[2]),
+ sizeof(int),
+ (void *)(& (d2.p[1])->arr[0]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_4,"Assertion","main",
+ "\\valid(&(d2.p[1])->arr[2])",
+ "tests/memory/array_overflow.c",43);
+ }
+ /*@ assert \valid(&(d2.p[1])->arr[2]); */ ;
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& d2));
+ __e_acsl_delete_block((void *)(& dd));
+ __e_acsl_delete_block((void *)(& d));
+ __e_acsl_delete_block((void *)(& ap));
+ __e_acsl_delete_block((void *)(a));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
index f8af717e7fc9df4d1b7eb04fc1bd52cc5b60962e..377558e4bf80b06d287aac2320ddf330d2929f88 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
@@ -85,7 +85,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),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid,"Assertion","main",
"\\valid((char **)_A)",
"tests/memory/compound_initializers.c",33);
@@ -150,7 +150,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),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_3,"Assertion","main",
"\\valid((int *)_D)",
"tests/memory/compound_initializers.c",38);
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c
index d3e4601ad639de99914601753a91ff8aa6ce462f..9e77764efee630d049fb0de3468fc7bd34117ee0 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c
@@ -65,7 +65,7 @@ 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),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","main",
"mem_access: \\valid_read(&t[2] - i)",
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 9e15dfb8febf6839dcddb1f65f9d0a7d19c24353..09b821c164e8d79554d2870d8f8e6c7833b51bb3 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
@@ -264,7 +264,7 @@ int main(void)
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)(& t3[6][1][0]) +
4 * 2),
(size_t)__gen_e_acsl_if_11,
- (void *)(& t3[6][1][0]),
+ (void *)(& t3[0][0][0]),
(void *)0);
__e_acsl_assert(! __gen_e_acsl_valid_read,"Assertion","main",
"!\\valid_read(&t3[6][1][0] + (2 .. 10))",
@@ -282,7 +282,7 @@ int main(void)
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& t3[__gen_e_acsl_range_3][1]),
sizeof(float [4]),
- (void *)(& t3[__gen_e_acsl_range_3][1]),
+ (void *)(& t3[0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_2) ;
else {
@@ -311,7 +311,7 @@ int main(void)
int __gen_e_acsl_valid_8;
__gen_e_acsl_valid_8 = __e_acsl_valid((void *)(& t4[4][__gen_e_acsl_range_4][2]),
sizeof(int),
- (void *)(& t4[4][__gen_e_acsl_range_4][2]),
+ (void *)(& t4[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_8) ;
else {
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 10644067af706030bda70f5b9223838e183558e8..e936c91164e729ca396f3396136ea0160eed2ef9 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
@@ -286,14 +286,14 @@ int main(void)
__gen_e_acsl_valid_read_14 = __e_acsl_valid_read((void *)(array),
sizeof(double),
(void *)(array),
- (void *)(array));
+ (void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read((double *)array); */
__e_acsl_assert(__gen_e_acsl_valid_read_14,"RTE","main",
"separated_guard: \\valid_read((double *)array)",
"tests/memory/separated.c",24);
__gen_e_acsl_valid_read_15 = __e_acsl_valid_read((void *)(& array[1]),
sizeof(double),
- (void *)(& array[1]),
+ (void *)(array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[1]); */
__e_acsl_assert(__gen_e_acsl_valid_read_15,"RTE","main",
@@ -966,7 +966,7 @@ int main(void)
int __gen_e_acsl_valid_read_41;
__gen_e_acsl_valid_read_41 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range][0]),
sizeof(double),
- (void *)(& array_1[0][__gen_e_acsl_range][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_41) ;
else {
@@ -991,7 +991,7 @@ int main(void)
int __gen_e_acsl_valid_read_42;
__gen_e_acsl_valid_read_42 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_2][0]),
sizeof(double),
- (void *)(& array_1[0][__gen_e_acsl_range_2][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_42) ;
else {
@@ -1016,7 +1016,7 @@ int main(void)
int __gen_e_acsl_valid_read_43;
__gen_e_acsl_valid_read_43 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_3][0]),
sizeof(double),
- (void *)(& array_1[0][__gen_e_acsl_range_3][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_43) ;
else {
@@ -1058,7 +1058,7 @@ int main(void)
int __gen_e_acsl_separated_19;
__gen_e_acsl_valid_read_44 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_6][0]),
sizeof(double),
- (void *)(& array_1[0][__gen_e_acsl_range_6][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
/*@ assert
E_ACSL: separated_guard:
@@ -1069,7 +1069,7 @@ int main(void)
"tests/memory/separated.c",60);
__gen_e_acsl_valid_read_45 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_5][0]),
sizeof(double),
- (void *)(& array_1[0][__gen_e_acsl_range_5][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
/*@ assert
E_ACSL: separated_guard:
@@ -1080,7 +1080,7 @@ int main(void)
"tests/memory/separated.c",60);
__gen_e_acsl_valid_read_46 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_4][0]),
sizeof(double),
- (void *)(& array_1[0][__gen_e_acsl_range_4][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
/*@ assert
E_ACSL: separated_guard:
@@ -1151,7 +1151,7 @@ int main(void)
int __gen_e_acsl_valid_read_47;
__gen_e_acsl_valid_read_47 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_7][0]),
sizeof(double),
- (void *)(& array_1[0][__gen_e_acsl_range_7][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_47) ;
else {
@@ -1176,7 +1176,7 @@ int main(void)
int __gen_e_acsl_valid_read_48;
__gen_e_acsl_valid_read_48 = __e_acsl_valid_read((void *)(& array_1[1][__gen_e_acsl_range_8][0]),
sizeof(double),
- (void *)(& array_1[1][__gen_e_acsl_range_8][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_48) ;
else {
@@ -1201,7 +1201,7 @@ int main(void)
int __gen_e_acsl_valid_read_49;
__gen_e_acsl_valid_read_49 = __e_acsl_valid_read((void *)(& array_1[2][__gen_e_acsl_range_9][0]),
sizeof(double),
- (void *)(& array_1[2][__gen_e_acsl_range_9][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_49) ;
else {
@@ -1243,7 +1243,7 @@ int main(void)
int __gen_e_acsl_separated_20;
__gen_e_acsl_valid_read_50 = __e_acsl_valid_read((void *)(& array_1[0][__gen_e_acsl_range_12][0]),
sizeof(double),
- (void *)(& array_1[0][__gen_e_acsl_range_12][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
/*@ assert
E_ACSL: separated_guard:
@@ -1254,7 +1254,7 @@ int main(void)
"tests/memory/separated.c",61);
__gen_e_acsl_valid_read_51 = __e_acsl_valid_read((void *)(& array_1[1][__gen_e_acsl_range_11][0]),
sizeof(double),
- (void *)(& array_1[1][__gen_e_acsl_range_11][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
/*@ assert
E_ACSL: separated_guard:
@@ -1265,7 +1265,7 @@ int main(void)
"tests/memory/separated.c",61);
__gen_e_acsl_valid_read_52 = __e_acsl_valid_read((void *)(& array_1[2][__gen_e_acsl_range_10][0]),
sizeof(double),
- (void *)(& array_1[2][__gen_e_acsl_range_10][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
/*@ assert
E_ACSL: separated_guard:
@@ -1341,7 +1341,7 @@ int main(void)
int __gen_e_acsl_valid_read_53;
__gen_e_acsl_valid_read_53 = __e_acsl_valid_read((void *)(& array_1[__gen_e_acsl_range_13][__gen_e_acsl_range_14][0]),
sizeof(double),
- (void *)(& array_1[__gen_e_acsl_range_13][__gen_e_acsl_range_14][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_53) ;
else {
@@ -1382,7 +1382,7 @@ int main(void)
int __gen_e_acsl_valid_read_54;
__gen_e_acsl_valid_read_54 = __e_acsl_valid_read((void *)(& array_1[__gen_e_acsl_range_15][__gen_e_acsl_range_16][0]),
sizeof(double),
- (void *)(& array_1[__gen_e_acsl_range_15][__gen_e_acsl_range_16][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_54) ;
else {
@@ -1439,9 +1439,7 @@ int main(void)
int __gen_e_acsl_separated_21;
__gen_e_acsl_valid_read_55 = __e_acsl_valid_read
((void *)(& array_1[__gen_e_acsl_range_19][__gen_e_acsl_range_20][0]),
- sizeof(double),
- (void *)(& array_1[__gen_e_acsl_range_19][__gen_e_acsl_range_20][0]),
- (void *)0);
+ sizeof(double),(void *)(& array_1[0][0][0]),(void *)0);
/*@ assert
E_ACSL: separated_guard:
\valid_read(&array_1[range_19][range_20][0]);
@@ -1452,9 +1450,7 @@ int main(void)
"tests/memory/separated.c",62);
__gen_e_acsl_valid_read_56 = __e_acsl_valid_read
((void *)(& array_1[__gen_e_acsl_range_17][__gen_e_acsl_range_18][0]),
- sizeof(double),
- (void *)(& array_1[__gen_e_acsl_range_17][__gen_e_acsl_range_18][0]),
- (void *)0);
+ sizeof(double),(void *)(& array_1[0][0][0]),(void *)0);
/*@ assert
E_ACSL: separated_guard:
\valid_read(&array_1[range_17][range_18][0]);
@@ -1534,7 +1530,7 @@ int main(void)
int __gen_e_acsl_valid_read_57;
__gen_e_acsl_valid_read_57 = __e_acsl_valid_read((void *)(& array_1[__gen_e_acsl_range_21][__gen_e_acsl_range_22][0]),
sizeof(double),
- (void *)(& array_1[__gen_e_acsl_range_21][__gen_e_acsl_range_22][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_57) ;
else {
@@ -1575,7 +1571,7 @@ int main(void)
int __gen_e_acsl_valid_read_58;
__gen_e_acsl_valid_read_58 = __e_acsl_valid_read((void *)(& array_1[__gen_e_acsl_range_23][__gen_e_acsl_range_24][0]),
sizeof(double),
- (void *)(& array_1[__gen_e_acsl_range_23][__gen_e_acsl_range_24][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_58) ;
else {
@@ -1632,9 +1628,7 @@ int main(void)
int __gen_e_acsl_separated_22;
__gen_e_acsl_valid_read_59 = __e_acsl_valid_read
((void *)(& array_1[__gen_e_acsl_range_27][__gen_e_acsl_range_28][0]),
- sizeof(double),
- (void *)(& array_1[__gen_e_acsl_range_27][__gen_e_acsl_range_28][0]),
- (void *)0);
+ sizeof(double),(void *)(& array_1[0][0][0]),(void *)0);
/*@ assert
E_ACSL: separated_guard:
\valid_read(&array_1[range_27][range_28][0]);
@@ -1645,9 +1639,7 @@ int main(void)
"tests/memory/separated.c",63);
__gen_e_acsl_valid_read_60 = __e_acsl_valid_read
((void *)(& array_1[__gen_e_acsl_range_25][__gen_e_acsl_range_26][0]),
- sizeof(double),
- (void *)(& array_1[__gen_e_acsl_range_25][__gen_e_acsl_range_26][0]),
- (void *)0);
+ sizeof(double),(void *)(& array_1[0][0][0]),(void *)0);
/*@ assert
E_ACSL: separated_guard:
\valid_read(&array_1[range_25][range_26][0]);
@@ -1732,7 +1724,7 @@ int main(void)
int __gen_e_acsl_valid_read_61;
__gen_e_acsl_valid_read_61 = __e_acsl_valid_read((void *)(& array_1[__gen_e_acsl_range_31][__gen_e_acsl_range_32][0]),
sizeof(double),
- (void *)(& array_1[__gen_e_acsl_range_31][__gen_e_acsl_range_32][0]),
+ (void *)(& array_1[0][0][0]),
(void *)0);
if (__gen_e_acsl_valid_read_61) ;
else {
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c
index ac348fd03d07fe972e9e5538f9ad71fea4efd51e..b41f84faf62fc4cded973dbb2f0c68656cec405f 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c
@@ -75,7 +75,7 @@ int main(void)
{
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)(& v1[2]),sizeof(int),
- (void *)(& v1[2]),(void *)0);
+ (void *)(v1),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid,"Assertion","main","\\valid(&v1[2])",
"tests/memory/vector.c",21);
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/array_overflow.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/array_overflow.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c
index ae17894128e01dbc6defcdf9c94589f425b62e21..e99bf6424a11e3c6dca10b17822de9acc653668d 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c
@@ -20,7 +20,7 @@ int main(int argc, char **argv)
__e_acsl_temporal_store_nblock((void *)(& p),(void *)((char *)addr));
p = (char *)addr;
__e_acsl_full_init((void *)(& p));
- __e_acsl_temporal_store_nblock((void *)(& p),(void *)0x123456);
+ __e_acsl_temporal_store_nblock((void *)(& p),(void *)((char *)0x123456));
p = (char *)0x123456;
__e_acsl_full_init((void *)(& p));
__e_acsl_temporal_store_nreferent((void *)(& p),(void *)(& q));
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
index 2d5749303a26b15e1ab2b9436ba2ec3a98e23413..f31a6b946fcf0328f911a77e459c17d52e5c77bf 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
@@ -10,7 +10,7 @@ void area_triangle(double (*vertices)[4])
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(*(vertices + 0)),
sizeof(double),
(void *)(*(vertices + 0)),
- (void *)(*(vertices + 0)));
+ (void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read,"Assertion","area_triangle",
"rte: mem_access: \\valid_read((double *)*(vertices + 0))",
"tests/temporal/t_darray.c",6);
@@ -21,7 +21,7 @@ void area_triangle(double (*vertices)[4])
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(*(vertices + 1)),
sizeof(double),
(void *)(*(vertices + 1)),
- (void *)(*(vertices + 1)));
+ (void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read_2,"Assertion","area_triangle",
"rte: mem_access: \\valid_read((double *)*(vertices + 1))",
"tests/temporal/t_darray.c",7);