From 739e3c8247af22d7f87dbc25df3356e4bb63dcd1 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 4 May 2020 16:26:32 +0200
Subject: [PATCH] [wp] Refacto on initialized load MemLoader
---
src/plugins/wp/MemLoader.ml | 23 ++-
.../wp/tests/wp_acsl/initialized_memtyped.i | 4 +-
.../assigned_initialized_memtyped.res.oracle | 172 +++++++++---------
.../oracle/initialized_memtyped.res.oracle | 135 +++++---------
.../0382f6dae0638cff22773abf48a97a0b.json | 2 +
.../3ea4d20271db817acc93772ec936b090.json | 2 +
.../4f12567037ded6ea1b91d0a3af02fb60.json | 2 +
.../67e6da20c960f8c39b37c0a80a14fc79.json | 2 +
.../7b438e920474037e0f9f8a713cb123c1.json | 2 +
.../7bd58c1c63463f3390d8763cb1b60289.json | 2 +
.../853bc2c32f8d7202db06cd790b63f160.json | 2 +
.../87784d16e7bf7c3e607493bd07398ff0.json | 2 +
.../88cebc928f7f09c8404f0f551912aac0.json | 1 +
.../ba3b33e2aa1b2fcd91adf55c7c60b152.json | 2 +
.../0c8d8229fd1113c3aaac6d045c5ec17a.json | 1 +
.../22d831911a6e3b613da9488f25950dfa.json | 1 +
.../45889d9c2cc0ab362df5992931e4e411.json | 1 +
.../5eb01b7fcbf37ae8cdb071894915cf4e.json | 1 +
.../743d15e7563acf247b9f2a22711598a4.json | 1 +
.../98d3ad4d3d19397488a568e130e4a373.json | 1 +
.../a3f6368cb0806f34fc5eb60b1a8eb93c.json | 1 +
.../af0d67d49865f04c3f4d3216185761aa.json | 1 +
.../d0bcf57829c78e344070c1106612dc8b.json | 1 +
.../d543dec067259b4ba816ad79e9be5b57.json | 1 +
.../d7a062a09dde68021c1bbec999efc80a.json | 2 +
.../fbb3088e2b317a17bfb09f485fab1a28.json | 1 +
.../initialized_memtyped.res.oracle | 12 +-
27 files changed, 177 insertions(+), 201 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/0382f6dae0638cff22773abf48a97a0b.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/3ea4d20271db817acc93772ec936b090.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/4f12567037ded6ea1b91d0a3af02fb60.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/67e6da20c960f8c39b37c0a80a14fc79.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/7b438e920474037e0f9f8a713cb123c1.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/7bd58c1c63463f3390d8763cb1b60289.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/853bc2c32f8d7202db06cd790b63f160.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/87784d16e7bf7c3e607493bd07398ff0.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/88cebc928f7f09c8404f0f551912aac0.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/ba3b33e2aa1b2fcd91adf55c7c60b152.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/0c8d8229fd1113c3aaac6d045c5ec17a.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/22d831911a6e3b613da9488f25950dfa.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/45889d9c2cc0ab362df5992931e4e411.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/5eb01b7fcbf37ae8cdb071894915cf4e.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/743d15e7563acf247b9f2a22711598a4.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/98d3ad4d3d19397488a568e130e4a373.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/a3f6368cb0806f34fc5eb60b1a8eb93c.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/af0d67d49865f04c3f4d3216185761aa.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d0bcf57829c78e344070c1106612dc8b.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d543dec067259b4ba816ad79e9be5b57.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d7a062a09dde68021c1bbec999efc80a.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/fbb3088e2b317a17bfb09f485fab1a28.json
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 3c05f23b3bc..f948bc49835 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -386,22 +386,24 @@ struct
(* --- Initialized --- *)
(* -------------------------------------------------------------------------- *)
- let rec initialized_term obj term =
+ let rec initialized_loc sigma obj loc =
match obj with
- | C_int _ | C_float _ | C_pointer _ -> p_bool term
+ | C_int _ | C_float _ | C_pointer _ ->
+ p_bool (initvalue sigma obj loc)
| C_comp ci ->
let initialized_field f =
- initialized_term
- (object_of f.ftype)
- (e_getfield term (Cfield (f, KInit)))
+ initialized_loc sigma (object_of f.ftype) (M.field loc f)
in
p_conj (List.map initialized_field ci.cfields)
| C_array ai ->
let obj_e, ds = Matrix.of_array ai in
let denv = Matrix.denv ds in
- let values = List.fold_left e_get term denv.index_val in
- let make_subst var value p =
- match value with
+ let access =
+ List.fold_left
+ (fun loc ofs -> M.shift loc obj_e ofs) loc denv.index_val
+ in
+ let make_subst var size p =
+ match size with
| None -> p
| Some i -> p_subst_var var (e_int i) p
in
@@ -410,10 +412,7 @@ struct
List.fold_left (fun p f -> f p) (p_conj denv.index_range) substs
in
p_forall denv.index_var
- (p_imply conj (initialized_term obj_e values))
-
- let initialized_loc sigma obj loc =
- initialized_term obj (initvalue sigma obj loc)
+ (p_imply conj (initialized_loc sigma obj_e access))
let initialized sigma = function
| Rloc(obj, loc) -> initialized_loc sigma obj loc
diff --git a/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i b/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
index 76148a465d8..91aa60d7152 100644
--- a/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
+++ b/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
@@ -39,7 +39,7 @@ void test(int* x, int (*a)[2], struct C* c){
//@ check unknown: \initialized(c);
c->s.y = 1 ;
- //@ check provable: \initialized(&c->s);
+ //@ check qed_ok: \initialized(&c->s);
//@ check unknown: \initialized(c);
c->a[0] = c->a[1] = c->a[2] = c->a[3] = c->a[4] = c->a[5] = c->a[6] = c->a[7] = c->a[8] = 1;
@@ -47,5 +47,5 @@ void test(int* x, int (*a)[2], struct C* c){
//@ check unknown: \initialized(c);
c->a[9] = 1 ;
- //@ check provable: \initialized(c);
+ //@ check qed_ok: \initialized(c);
}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
index d9d2221b18f..c3bdcf83e16 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
@@ -13,31 +13,30 @@ Let a = shiftfield_F1_S_a(s).
Let a_1 = shift_sint32(a, 0).
Let a_2 = havoc(Init_undef_1, m, a_1, 10).
Let a_3 = havoc(Init_undef_0, m, a_1, 10).
-Let a_4 = Load_Init_S1_S(s, a_3).
Assume {
- Type: is_sint32(i) /\ is_sint32(i_1).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_sint32(i_1) /\ is_sint32(i_2).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall i_2 : Z. let a_5 = shift_sint32(a, i_2) in ((0 <= i_2) ->
- ((i_2 <= 9) -> ((m[a_5]=true) -> (a_2[a_5]=true)))).
+ Have: forall i_3 : Z. let a_4 = shift_sint32(a, i_3) in ((0 <= i_3) ->
+ ((i_3 <= 9) -> ((m[a_4]=true) -> (a_2[a_4]=true)))).
(* Invariant *)
- Have: (0 <= i) /\ (i <= 10) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_2[shift_sint32(a, i_2)]=true)))).
+ Have: (0 <= i_1) /\ (i_1 <= 10) /\
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
+ (a_2[shift_sint32(a, i_3)]=true)))).
(* Else *)
- Have: 10 <= i.
+ Have: 10 <= i_1.
(* Loop assigns 'CHECK' *)
- Have: forall i_2 : Z. let a_5 = shift_sint32(a, i_2) in ((0 <= i_2) ->
- ((i_2 <= 9) -> ((a_2[a_5]=true) -> (a_3[a_5]=true)))).
+ Have: forall i_3 : Z. let a_4 = shift_sint32(a, i_3) in ((0 <= i_3) ->
+ ((i_3 <= 9) -> ((a_2[a_4]=true) -> (a_3[a_4]=true)))).
(* Invariant *)
- Have: (0 <= i_1) /\ (i_1 <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i_2.
}
-Prove: ((a_4.Init_F1_S_i)=true) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
- ((a_4.Init_F1_S_a)[i_2]=true)))).
+Prove: (a_3[shift_sint32(a, i)]=true).
------------------------------------------------------------
@@ -62,34 +61,34 @@ Prove: true.
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 118):
-Let m = Init_0[shiftfield_F1_S_i(s) <- true].
-Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_1, m, shift_sint32(a, 0), 10).
-Let a_2 = havoc(Init_undef_0, m, s, 11).
-Let a_3 = Load_Init_S1_S(s, a_2).
+Let a = shiftfield_F1_S_i(s).
+Let m = Init_0[a <- true].
+Let a_1 = shiftfield_F1_S_a(s).
+Let a_2 = havoc(Init_undef_1, m, shift_sint32(a_1, 0), 10).
+Let a_3 = havoc(Init_undef_0, m, s, 11).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall i_2 : Z. let a_4 = shift_sint32(a, i_2) in ((0 <= i_2) ->
- ((i_2 <= 9) -> ((m[a_4]=true) -> (a_1[a_4]=true)))).
+ Have: forall i_2 : Z. let a_4 = shift_sint32(a_1, i_2) in ((0 <= i_2) ->
+ ((i_2 <= 9) -> ((m[a_4]=true) -> (a_2[a_4]=true)))).
(* Invariant *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_1[shift_sint32(a, i_2)]=true)))).
+ (a_2[shift_sint32(a_1, i_2)]=true)))).
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: Motononic__Init_S1_S(s, a_1, a_2).
+ Have: Motononic__Init_S1_S(s, a_2, a_3).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *)
Have: 10 <= i_1.
}
-Prove: ((a_3.Init_F1_S_i)=true) /\
+Prove: (Init_undef_0[a]=true) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
- ((a_3.Init_F1_S_a)[i_2]=true)))).
+ (a_3[shift_sint32(a_1, i_2)]=true)))).
------------------------------------------------------------
@@ -144,14 +143,13 @@ Let a_1 = shiftfield_F1_S_i(s).
Let m = Init_1[a_1 <- true].
Let a_2 = shift_sint32(a, 0).
Let a_3 = havoc(Init_undef_0, m, a_2, 10).
-Let a_4 = Load_Init_S1_S(s, Init_0).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall i_2 : Z. let a_5 = shift_sint32(a, i_2) in ((0 <= i_2) ->
- ((i_2 <= 9) -> ((m[a_5]=true) -> (a_3[a_5]=true)))).
+ Have: forall i_2 : Z. let a_4 = shift_sint32(a, i_2) in ((0 <= i_2) ->
+ ((i_2 <= 9) -> ((m[a_4]=true) -> (a_3[a_4]=true)))).
(* Invariant *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
@@ -159,23 +157,23 @@ Assume {
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: (forall a_5 : addr.
+ Have: (forall a_4 : addr.
((forall i_2 : Z. (((i_2 = 0) \/ (i_2 = 2) \/ (i_2 = 4)) ->
- (shift_sint32(a, i_2) != a_5))) ->
- ((a_3[a_5]=true) <-> (Init_0[a_5]=true)))) /\
- (forall a_5 : addr.
+ (shift_sint32(a, i_2) != a_4))) ->
+ ((a_3[a_4]=true) <-> (Init_0[a_4]=true)))) /\
+ (forall a_4 : addr.
((forall i_2 : Z. (((i_2 = 0) \/ (i_2 = 2) \/ (i_2 = 4)) ->
- (shift_sint32(a, i_2) != a_5))) ->
- (havoc(Mint_undef_0, Mint_0[a_1 <- 0], a_2, 10)[a_5] = Mint_1[a_5]))) /\
- (forall i_2 : Z. let a_5 = shift_sint32(a, i_2) in
- (((i_2 = 0) \/ (i_2 = 2) \/ (i_2 = 4)) -> ((a_3[a_5]=true) ->
- (Init_0[a_5]=true)))).
+ (shift_sint32(a, i_2) != a_4))) ->
+ (havoc(Mint_undef_0, Mint_0[a_1 <- 0], a_2, 10)[a_4] = Mint_1[a_4]))) /\
+ (forall i_2 : Z. let a_4 = shift_sint32(a, i_2) in
+ (((i_2 = 0) \/ (i_2 = 2) \/ (i_2 = 4)) -> ((a_3[a_4]=true) ->
+ (Init_0[a_4]=true)))).
(* Else *)
Have: 10 <= i_1.
}
-Prove: ((a_4.Init_F1_S_i)=true) /\
+Prove: (Init_0[a_1]=true) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
- ((a_4.Init_F1_S_a)[i_2]=true)))).
+ (Init_0[shift_sint32(a, i_2)]=true)))).
------------------------------------------------------------
@@ -254,26 +252,25 @@ Let a = shiftfield_F1_S_i(s).
Let m = Init_0[a <- true].
Let a_1 = shiftfield_F1_S_a(s).
Let a_2 = havoc(Init_undef_0, m, shift_sint32(a_1, 0), 10).
-Let a_3 = Load_Init_S1_S(s, a_2[a <- true]).
Assume {
- Type: is_sint32(i) /\ is_sint32(i_1).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_sint32(i_1) /\ is_sint32(i_2).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall i_2 : Z. let a_4 = shift_sint32(a_1, i_2) in ((0 <= i_2) ->
- ((i_2 <= 9) -> ((m[a_4]=true) -> (a_2[a_4]=true)))).
+ Have: forall i_3 : Z. let a_3 = shift_sint32(a_1, i_3) in ((0 <= i_3) ->
+ ((i_3 <= 9) -> ((m[a_3]=true) -> (a_2[a_3]=true)))).
(* Invariant *)
- Have: (0 <= i) /\ (i <= 10) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_2[shift_sint32(a_1, i_2)]=true)))).
- (* Else *)
- Have: 10 <= i.
+ Have: (0 <= i_1) /\ (i_1 <= 10) /\
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
+ (a_2[shift_sint32(a_1, i_3)]=true)))).
(* Else *)
Have: 10 <= i_1.
+ (* Else *)
+ Have: 10 <= i_2.
}
-Prove: ((a_3.Init_F1_S_i)=true) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
- ((a_3.Init_F1_S_a)[i_2]=true)))).
+Prove: (a_2[a <- true][shift_sint32(a_1, i)]=true).
------------------------------------------------------------
@@ -296,28 +293,27 @@ Let a = shiftfield_F1_S_a(s).
Let a_1 = shift_sint32(a, 4).
Let m = Init_0[shiftfield_F1_S_i(s) <- true].
Let a_2 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
-Let a_3 = Load_Init_S1_S(s, a_2[a_1 <- i]).
Assume {
- Type: is_sint32(i_1) /\ is_sint32(i_2).
+ Have: 0 <= i_1.
+ Have: i_1 <= 9.
+ Type: is_sint32(i_2) /\ is_sint32(i_3).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall i_3 : Z. let a_4 = shift_sint32(a, i_3) in ((0 <= i_3) ->
- ((i_3 <= 9) -> ((m[a_4]=true) -> (a_2[a_4]=true)))).
+ Have: forall i_4 : Z. let a_3 = shift_sint32(a, i_4) in ((0 <= i_4) ->
+ ((i_4 <= 9) -> ((m[a_3]=true) -> (a_2[a_3]=true)))).
(* Invariant *)
- Have: (0 <= i_1) /\ (i_1 <= 10) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
- (a_2[shift_sint32(a, i_3)]=true)))).
+ Have: (0 <= i_2) /\ (i_2 <= 10) /\
+ (forall i_4 : Z. ((0 <= i_4) -> ((i_4 < i_2) ->
+ (a_2[shift_sint32(a, i_4)]=true)))).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i_2.
(* Loop assigns 'CHECK' *)
Have: ((Init_undef_0[a_1]=true) -> (i=true)).
(* Else *)
- Have: 10 <= i_2.
+ Have: 10 <= i_3.
}
-Prove: ((a_3.Init_F1_S_i)=true) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- ((a_3.Init_F1_S_a)[i_3]=true)))).
+Prove: (a_2[a_1 <- i][shift_sint32(a, i_1)]=true).
------------------------------------------------------------
@@ -374,24 +370,23 @@ Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 21)
Let m = Init_0[shiftfield_F1_S_i(s) <- true].
Let a = shiftfield_F1_S_a(s).
Let a_1 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
-Let a_2 = Load_Init_S1_S(s, a_1).
Assume {
- Type: is_sint32(i).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_sint32(i_1).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns 'CHECK' *)
- Have: forall i_1 : Z. let a_3 = shift_sint32(a, i_1) in ((0 <= i_1) ->
- ((i_1 <= 9) -> ((m[a_3]=true) -> (a_1[a_3]=true)))).
+ Have: forall i_2 : Z. let a_2 = shift_sint32(a, i_2) in ((0 <= i_2) ->
+ ((i_2 <= 9) -> ((m[a_2]=true) -> (a_1[a_2]=true)))).
(* Invariant 'CHECK' *)
- Have: (0 <= i) /\ (i <= 10) /\
- (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_1[shift_sint32(a, i_1)]=true)))).
+ Have: (0 <= i_1) /\ (i_1 <= 10) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
+ (a_1[shift_sint32(a, i_2)]=true)))).
(* Else *)
- Have: 10 <= i.
+ Have: 10 <= i_1.
}
-Prove: ((a_2.Init_F1_S_i)=true) /\
- (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) ->
- ((a_2.Init_F1_S_a)[i_1]=true)))).
+Prove: (a_1[shift_sint32(a, i)]=true).
------------------------------------------------------------
@@ -420,29 +415,28 @@ Let m = Init_0[shiftfield_F1_S_i(s) <- true].
Let a = shiftfield_F1_S_a(s).
Let a_1 = havoc(Init_undef_1, m, shift_sint32(a, 0), 10).
Let a_2 = havoc(Init_undef_0, a_1, shift_sint32(a, 1), 4).
-Let a_3 = Load_Init_S1_S(s, a_2).
Assume {
- Type: is_sint32(i) /\ is_sint32(i_1).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_sint32(i_1) /\ is_sint32(i_2).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall i_2 : Z. let a_4 = shift_sint32(a, i_2) in ((0 <= i_2) ->
- ((i_2 <= 9) -> ((m[a_4]=true) -> (a_1[a_4]=true)))).
+ Have: forall i_3 : Z. let a_3 = shift_sint32(a, i_3) in ((0 <= i_3) ->
+ ((i_3 <= 9) -> ((m[a_3]=true) -> (a_1[a_3]=true)))).
(* Invariant *)
- Have: (0 <= i) /\ (i <= 10) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_1[shift_sint32(a, i_2)]=true)))).
+ Have: (0 <= i_1) /\ (i_1 <= 10) /\
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
+ (a_1[shift_sint32(a, i_3)]=true)))).
(* Else *)
- Have: 10 <= i.
+ Have: 10 <= i_1.
(* Loop assigns 'CHECK' *)
- Have: forall i_2 : Z. let a_4 = shift_sint32(a, i_2) in ((0 < i_2) ->
- ((i_2 <= 4) -> ((a_1[a_4]=true) -> (a_2[a_4]=true)))).
+ Have: forall i_3 : Z. let a_3 = shift_sint32(a, i_3) in ((0 < i_3) ->
+ ((i_3 <= 4) -> ((a_1[a_3]=true) -> (a_2[a_3]=true)))).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i_2.
}
-Prove: ((a_3.Init_F1_S_i)=true) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
- ((a_3.Init_F1_S_a)[i_2]=true)))).
+Prove: (a_2[shift_sint32(a, i)]=true).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
index a3d7ea7b5a0..a68ba3f09fd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
@@ -20,17 +20,18 @@ Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 1).
}
-Prove: (ArrayInit1_int(a, 2, Init_0)[i]=true).
+Prove: (Init_0[shift_sint32(a, i)]=true).
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 14):
-Let a = Load_Init_S2_C(c, Init_0).
-Let a_1 = a.Init_F2_C_s.
+Let a = shiftfield_F2_C_s(c).
Assume { (* Heap *) Type: region(c.base) <= 0. }
-Prove: ((a.Init_F2_C_x)=true) /\ ((a_1.Init_F1_S_x)=true) /\
- ((a_1.Init_F1_S_y)=true) /\
- (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a.Init_F2_C_a)[i]=true)))).
+Prove: (Init_0[shiftfield_F2_C_x(c)]=true) /\
+ (Init_0[shiftfield_F1_S_x(a)]=true) /\
+ (Init_0[shiftfield_F1_S_y(a)]=true) /\
+ (forall i : Z. ((0 <= i) -> ((i <= 9) ->
+ (Init_0[shift_sint32(shiftfield_F2_C_a(c), i)]=true)))).
------------------------------------------------------------
@@ -57,8 +58,7 @@ Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 1).
}
-Prove: (ArrayInit1_int(a, 2, Init_0[x <- true][shift_sint32(a, 0) <- true])
- [i]=true).
+Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, i)]=true).
------------------------------------------------------------
@@ -83,15 +83,15 @@ Prove: true.
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 31):
-Let a_1 = Load_Init_S1_S(shiftfield_F2_C_s(c),
- Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F2_C_x(c) <- true]).
+Let m = Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true].
+Let a_1 = shiftfield_F2_C_s(c).
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: ((a_1.Init_F1_S_x)=true) /\ ((a_1.Init_F1_S_y)=true).
+Prove: (m[shiftfield_F1_S_x(a_1)]=true) /\ (m[shiftfield_F1_S_y(a_1)]=true).
------------------------------------------------------------
@@ -103,25 +103,25 @@ Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 9).
}
-Prove: (ArrayInit1_int(shiftfield_F2_C_a(c), 10,
- Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F2_C_x(c) <- true])[i]=true).
+Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F2_C_x(c) <- true]
+ [shift_sint32(shiftfield_F2_C_a(c), i)]=true).
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 33):
-Let a_1 = Load_Init_S2_C(c,
- Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F2_C_x(c) <- true]).
-Let a_2 = a_1.Init_F2_C_s.
+Let m = Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true].
+Let a_1 = shiftfield_F2_C_s(c).
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: ((a_1.Init_F2_C_x)=true) /\ ((a_2.Init_F1_S_x)=true) /\
- ((a_2.Init_F1_S_y)=true) /\
- (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a_1.Init_F2_C_a)[i]=true)))).
+Prove: (m[shiftfield_F1_S_x(a_1)]=true) /\
+ (m[shiftfield_F1_S_y(a_1)]=true) /\
+ (forall i : Z. ((0 <= i) -> ((i <= 9) ->
+ (m[shiftfield_F2_C_x(c) <- true][shift_sint32(shiftfield_F2_C_a(c), i)]=true)))).
------------------------------------------------------------
@@ -142,67 +142,50 @@ Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 38):
-Let a_1 = shiftfield_F2_C_s(c).
-Let a_2 = Load_Init_S1_S(a_1,
- Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
- <- true]).
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: ((a_2.Init_F1_S_x)=true) /\ ((a_2.Init_F1_S_y)=true).
+Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F1_S_y(shiftfield_F2_C_s(c))]=true).
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 39):
-Let a_1 = Load_Init_S2_C(c,
- Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F2_C_x(c) <- true]
- [shiftfield_F1_S_x(shiftfield_F2_C_s(c)) <- true]).
-Let a_2 = a_1.Init_F2_C_s.
+Let m = Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true].
+Let a_1 = shiftfield_F2_C_s(c).
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: ((a_1.Init_F2_C_x)=true) /\ ((a_2.Init_F1_S_x)=true) /\
- ((a_2.Init_F1_S_y)=true) /\
- (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a_1.Init_F2_C_a)[i]=true)))).
+Prove: (m[shiftfield_F1_S_y(a_1)]=true) /\
+ (forall i : Z. ((0 <= i) -> ((i <= 9) ->
+ (m[shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1) <- true]
+ [shift_sint32(shiftfield_F2_C_a(c), i)]=true)))).
------------------------------------------------------------
-Goal Check 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 42):
-Let a_1 = shiftfield_F2_C_s(c).
-Let a_2 = Load_Init_S1_S(a_1,
- Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
- <- true][shiftfield_F1_S_y(a_1) <- true]).
-Assume {
- (* Heap *)
- Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
- (region(x.base) <= 0).
-}
-Prove: ((a_2.Init_F1_S_x)=true) /\ ((a_2.Init_F1_S_y)=true).
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 42):
+Prove: true.
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 43):
Let a_1 = shiftfield_F2_C_s(c).
-Let a_2 = Load_Init_S2_C(c,
- Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
- <- true][shiftfield_F1_S_y(a_1) <- true]).
-Let a_3 = a_2.Init_F2_C_s.
Assume {
+ Have: 0 <= i.
+ Have: i <= 9.
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: ((a_2.Init_F2_C_x)=true) /\ ((a_3.Init_F1_S_x)=true) /\
- ((a_3.Init_F1_S_y)=true) /\
- (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a_2.Init_F2_C_a)[i]=true)))).
+Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+ <- true][shiftfield_F1_S_y(a_1) <- true]
+ [shift_sint32(shiftfield_F2_C_a(c), i)]=true).
------------------------------------------------------------
@@ -228,49 +211,17 @@ Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 47):
-Let a_1 = shiftfield_F2_C_s(c).
-Let a_2 = shiftfield_F2_C_a(c).
-Let a_3 = Load_Init_S2_C(c,
- Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
- <- true][shiftfield_F1_S_y(a_1) <- true][shift_sint32(a_2, 8)
- <- true][shift_sint32(a_2, 7) <- true][shift_sint32(a_2, 6)
- <- true][shift_sint32(a_2, 5) <- true][shift_sint32(a_2, 4)
- <- true][shift_sint32(a_2, 3) <- true][shift_sint32(a_2, 2)
- <- true][shift_sint32(a_2, 1) <- true][shift_sint32(a_2, 0)
- <- true]).
-Let a_4 = a_3.Init_F2_C_s.
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: ((a_3.Init_F2_C_x)=true) /\ ((a_4.Init_F1_S_x)=true) /\
- ((a_4.Init_F1_S_y)=true) /\
- (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a_3.Init_F2_C_a)[i]=true)))).
+Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shift_sint32(shiftfield_F2_C_a(c), 9)]=true).
------------------------------------------------------------
-Goal Check 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 50):
-Let a_1 = shiftfield_F2_C_s(c).
-Let a_2 = shiftfield_F2_C_a(c).
-Let a_3 = Load_Init_S2_C(c,
- Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
- <- true][shiftfield_F1_S_y(a_1) <- true][shift_sint32(a_2, 8)
- <- true][shift_sint32(a_2, 7) <- true][shift_sint32(a_2, 6)
- <- true][shift_sint32(a_2, 5) <- true][shift_sint32(a_2, 4)
- <- true][shift_sint32(a_2, 3) <- true][shift_sint32(a_2, 2)
- <- true][shift_sint32(a_2, 1) <- true][shift_sint32(a_2, 0)
- <- true][shift_sint32(a_2, 9) <- true]).
-Let a_4 = a_3.Init_F2_C_s.
-Assume {
- (* Heap *)
- Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
- (region(x.base) <= 0).
-}
-Prove: ((a_3.Init_F2_C_x)=true) /\ ((a_4.Init_F1_S_x)=true) /\
- ((a_4.Init_F1_S_y)=true) /\
- (forall i : Z. ((0 <= i) -> ((i <= 9) -> ((a_3.Init_F2_C_a)[i]=true)))).
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 50):
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/0382f6dae0638cff22773abf48a97a0b.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/0382f6dae0638cff22773abf48a97a0b.json
new file mode 100644
index 00000000000..cb87c7c0d5c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/0382f6dae0638cff22773abf48a97a0b.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0134,
+ "steps": 21 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/3ea4d20271db817acc93772ec936b090.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/3ea4d20271db817acc93772ec936b090.json
new file mode 100644
index 00000000000..1e149c90f5c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/3ea4d20271db817acc93772ec936b090.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0074,
+ "steps": 20 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/4f12567037ded6ea1b91d0a3af02fb60.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/4f12567037ded6ea1b91d0a3af02fb60.json
new file mode 100644
index 00000000000..cd20d8ef7d4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/4f12567037ded6ea1b91d0a3af02fb60.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0125,
+ "steps": 31 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/67e6da20c960f8c39b37c0a80a14fc79.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/67e6da20c960f8c39b37c0a80a14fc79.json
new file mode 100644
index 00000000000..f5767b366bd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/67e6da20c960f8c39b37c0a80a14fc79.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.011,
+ "steps": 41 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/7b438e920474037e0f9f8a713cb123c1.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/7b438e920474037e0f9f8a713cb123c1.json
new file mode 100644
index 00000000000..c114478a6ec
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/7b438e920474037e0f9f8a713cb123c1.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.007,
+ "steps": 34 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/7bd58c1c63463f3390d8763cb1b60289.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/7bd58c1c63463f3390d8763cb1b60289.json
new file mode 100644
index 00000000000..b153fc44ecf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/7bd58c1c63463f3390d8763cb1b60289.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0074,
+ "steps": 16 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/853bc2c32f8d7202db06cd790b63f160.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/853bc2c32f8d7202db06cd790b63f160.json
new file mode 100644
index 00000000000..9e5ed808f80
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/853bc2c32f8d7202db06cd790b63f160.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0077,
+ "steps": 19 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/87784d16e7bf7c3e607493bd07398ff0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/87784d16e7bf7c3e607493bd07398ff0.json
new file mode 100644
index 00000000000..5139c3d8c4c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/87784d16e7bf7c3e607493bd07398ff0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0072,
+ "steps": 17 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/88cebc928f7f09c8404f0f551912aac0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/88cebc928f7f09c8404f0f551912aac0.json
new file mode 100644
index 00000000000..f1c71a09f6f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/88cebc928f7f09c8404f0f551912aac0.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.02, "steps": 91 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/ba3b33e2aa1b2fcd91adf55c7c60b152.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/ba3b33e2aa1b2fcd91adf55c7c60b152.json
new file mode 100644
index 00000000000..ef3ecf82401
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session/cache/ba3b33e2aa1b2fcd91adf55c7c60b152.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0098,
+ "steps": 66 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/0c8d8229fd1113c3aaac6d045c5ec17a.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/0c8d8229fd1113c3aaac6d045c5ec17a.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/0c8d8229fd1113c3aaac6d045c5ec17a.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/22d831911a6e3b613da9488f25950dfa.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/22d831911a6e3b613da9488f25950dfa.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/22d831911a6e3b613da9488f25950dfa.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/45889d9c2cc0ab362df5992931e4e411.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/45889d9c2cc0ab362df5992931e4e411.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/45889d9c2cc0ab362df5992931e4e411.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/5eb01b7fcbf37ae8cdb071894915cf4e.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/5eb01b7fcbf37ae8cdb071894915cf4e.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/5eb01b7fcbf37ae8cdb071894915cf4e.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/743d15e7563acf247b9f2a22711598a4.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/743d15e7563acf247b9f2a22711598a4.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/743d15e7563acf247b9f2a22711598a4.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/98d3ad4d3d19397488a568e130e4a373.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/98d3ad4d3d19397488a568e130e4a373.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/98d3ad4d3d19397488a568e130e4a373.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/a3f6368cb0806f34fc5eb60b1a8eb93c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/a3f6368cb0806f34fc5eb60b1a8eb93c.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/a3f6368cb0806f34fc5eb60b1a8eb93c.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/af0d67d49865f04c3f4d3216185761aa.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/af0d67d49865f04c3f4d3216185761aa.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/af0d67d49865f04c3f4d3216185761aa.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d0bcf57829c78e344070c1106612dc8b.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d0bcf57829c78e344070c1106612dc8b.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d0bcf57829c78e344070c1106612dc8b.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d543dec067259b4ba816ad79e9be5b57.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d543dec067259b4ba816ad79e9be5b57.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d543dec067259b4ba816ad79e9be5b57.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d7a062a09dde68021c1bbec999efc80a.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d7a062a09dde68021c1bbec999efc80a.json
new file mode 100644
index 00000000000..d0d5f44b1cf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/d7a062a09dde68021c1bbec999efc80a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1426,
+ "steps": 11 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/fbb3088e2b317a17bfb09f485fab1a28.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/fbb3088e2b317a17bfb09f485fab1a28.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session/cache/fbb3088e2b317a17bfb09f485fab1a28.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
index b27ea93eec7..f0add8dd99f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
@@ -22,15 +22,15 @@
[wp] [Alt-Ergo] Goal typed_test_check_unknown_9 : Unsuccess
[wp] [Alt-Ergo] Goal typed_test_check_unknown_10 : Unsuccess
[wp] [Alt-Ergo] Goal typed_test_check_unknown_11 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_test_check_provable : Valid
+[wp] [Qed] Goal typed_test_check_qed_ok_8 : Valid
[wp] [Alt-Ergo] Goal typed_test_check_unknown_12 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_test_check_provable_2 : Valid
+[wp] [Alt-Ergo] Goal typed_test_check_provable : Valid
[wp] [Alt-Ergo] Goal typed_test_check_unknown_13 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_test_check_provable_3 : Valid
+[wp] [Qed] Goal typed_test_check_qed_ok_9 : Valid
[wp] Proved goals: 10 / 23
- Qed: 7
- Alt-Ergo: 3 (unsuccess: 13)
+ Qed: 9
+ Alt-Ergo: 1 (unsuccess: 13)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- test 7 3 23 43.5%
+ test 9 1 23 43.5%
------------------------------------------------------------
--
GitLab