From 773171f4e33ac10befdb54a97f207d3b055f70fb Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 25 Jan 2019 11:13:58 +0100
Subject: [PATCH] [Wp] review of partial initializers
---
src/plugins/wp/CodeSemantics.ml | 93 +++---
src/plugins/wp/tests/wp_acsl/init_value.i | 31 +-
.../tests/wp_acsl/init_value.i.0.report.json | 44 ++-
.../tests/wp_acsl/init_value.i.1.report.json | 58 +++-
.../wp_acsl/oracle/init_value.0.res.oracle | 281 ++++++++++++++++++
.../wp_acsl/oracle/init_value.1.res.oracle | 136 +++++++++
.../oracle_qualif/init_value.0.res.oracle | 16 +-
.../oracle_qualif/init_value.1.res.oracle | 19 +-
8 files changed, 615 insertions(+), 63 deletions(-)
diff --git a/src/plugins/wp/CodeSemantics.ml b/src/plugins/wp/CodeSemantics.ml
index e1979163b85..fff974eeee8 100644
--- a/src/plugins/wp/CodeSemantics.ml
+++ b/src/plugins/wp/CodeSemantics.ml
@@ -469,18 +469,17 @@ struct
| CompoundInit ( ct , initl ) ->
let ct = constfold_ctyp ct in
- let len = List.length initl in
let acc = (* updated acc with default init of structure *)
match ct with
| TComp (cp,_,_) when cp.cstruct &&
- len < (List.length cp.cfields) ->
+ (List.length initl) < (List.length cp.cfields) ->
(* default init for unintialized field of a struct *)
List.fold_left
(fun acc f ->
if List.exists
(function
| Field(g,_),_ -> Fieldinfo.equal f g
- | _ -> false)
+ | _ -> WpLog.fatal "Kernel invariant broken into an initializer")
initl
then acc
else
@@ -495,70 +494,72 @@ struct
in
match ct with
| TArray (ty,len,_,_) ->
- let len = (* number of required elements *)
- match len with
- | Some {enode = (Const CInt64 (size,_,_))} -> size
- | Some len ->
- WpLog.fatal "Non-constant expression (%a) for an array size"
- Printer.pp_exp len
- | _ -> WpLog.fatal "Undefined array size"
+ let delayed =
+ match len with (* number of required elements *)
+ | Some {enode = (Const CInt64 (size,_,_))} ->
+ Some (size, None)
+ | _ -> None
in
- (* delayed: the last consecutive index have the same value
- and are not yet initialized.
- (i0,pred,il) =def \forall x. x \in [il;i0] t[x] == pred
- *)
+ (* delayed contents info about the last consecutive indices having
+ the same value, but that have not yet initialized. *)
let make_quant acc = function
- | None -> acc
- | Some (Index({enode=Const (CInt64 (i0,_,_))}, NoOffset),exp,il)
- when Integer.lt il i0 ->
+ | None -> acc (* nothing was delayed *)
+ | Some (_,None) -> acc (* nothing was delayed *)
+ | Some (il,Some (i0,_,exp)) when Integer.lt il i0 ->
+ (* \forall i \in [il .. i0] ; t[i]==exp *)
let i2 = Integer.succ i0 in
init_range ~sigma lv ty il i2 (Some exp) :: acc
- | Some (off,exp,_) ->
+ | Some (_il,Some (_i0,off,exp)) -> (* case _il=_i0 *)
let lv = Cil.addOffsetLval off lv in
init_value ~sigma lv ty (Some exp) :: acc
in
- let add_missing_indexes acc i0 i1 =
- if Integer.lt i1 i0 then acc
- else
- init_range ~sigma lv ty i0 i1 None :: acc
+ let add_missing_indices acc i0 = function
+ | Some (i1, _) ->
+ if Integer.ge i0 i1 then (* no hole *) acc
+ else (* defaults values *)
+ init_range ~sigma lv ty i0 i1 None :: acc
+ | _ -> (* last bound is unknown. *) acc
in
- let pos, acc, delayed =
+ let acc, delayed =
List.fold_left
- (fun (pos,acc,delayed) (off,init) ->
+ (fun (acc,delayed) (off,init) ->
let off = constfold_coffset off in
- let idx = match off with
- | Index({enode=Const (CInt64 (idx,_,_))}, _) ->
- if Integer.lt pos idx then
- WpLog.fatal "Unordered initializer";
- idx
- | Index(idx, _) ->
- WpLog.fatal "Non-constant index (%a) into an initializer"
- Printer.pp_exp idx
- | _ -> WpLog.fatal "Kernel invariant broken into an initializer"
+ let idx,acc = match off with
+ | Index({enode=Const CInt64 (idx,_,_)}, _) ->
+ (match delayed with
+ | Some (iprev, _) when Integer.lt iprev idx ->
+ (* an algo with a 2sd pass is required
+ for introducing default values *)
+ WpLog.fatal "Unordered initializer";
+ | _ -> ()) ;
+ Some (idx,None), (* adds eventual default values *)
+ add_missing_indices acc (Integer.succ idx) delayed
+ | _ -> None,acc
in
- let acc = add_missing_indexes acc (Integer.succ idx) pos in
- match off, init with
- | Index(_,NoOffset), SingleInit curr -> begin
+ match idx, off, init with
+ | Some (idx,_), Index(_, NoOffset), SingleInit init -> begin
match delayed with
- | None -> idx,acc,Some(off,curr,idx)
- | Some (i0,prev,ip)
+ | None -> acc,Some (idx,Some(idx,off,init))
+ | Some (i_prev,(Some (_,_,init_delayed) as delayed_info))
when Wp_parameters.InitWithForall.get ()
- && Integer.equal (Integer.pred ip) idx
- && ExpStructEq.equal prev curr ->
- idx,acc,Some(i0,prev,idx)
+ && Integer.equal (Integer.pred i_prev) idx
+ && ExpStructEq.equal init_delayed init ->
+ acc,Some (idx,delayed_info)
| _ ->
let acc = make_quant acc delayed in
- idx, acc, Some (off,curr,idx)
+ acc, Some (idx, Some (idx,off,init))
end
- | _ ->
+ | _, Index(_, _),_ ->
+ let acc = make_quant acc delayed in
let lv = Cil.addOffsetLval off lv in
- idx, (init_variable ~sigma lv init acc), None
+ (init_variable ~sigma lv init acc), idx
+ | _ -> WpLog.fatal "Kernel invariant broken into an initializer"
)
- (len,acc,None)
+ (acc,delayed)
(List.rev initl)
in
let acc = make_quant acc delayed in
- add_missing_indexes acc Integer.zero pos
+ add_missing_indices acc Integer.zero delayed
| _ ->
List.fold_left
(fun acc (off,init) ->
diff --git a/src/plugins/wp/tests/wp_acsl/init_value.i b/src/plugins/wp/tests/wp_acsl/init_value.i
index 1f555a15daa..b9d9caeabad 100644
--- a/src/plugins/wp/tests/wp_acsl/init_value.i
+++ b/src/plugins/wp/tests/wp_acsl/init_value.i
@@ -1,9 +1,9 @@
/* run.config
- OPT: -wp-no-let
+ OPT: -wp-init-const -wp-no-let
OPT: -main main_ko -wp-no-let
*/
/* run.config_qualif
- OPT: -wp -wp-par 1 -wp-prop="-qed_ko"
+ OPT: -wp-init-const -wp -wp-par 1 -wp-prop="-qed_ko"
OPT: -main main_ko -wp-par 1 -wp-prop qed_ko -wp-steps 50
*/
@@ -25,7 +25,7 @@ struct Sc {int a; int b[2+1]; int c;};
struct Sc sc0 = {1,{2,3,4},5};
struct Sc sc1 = {1,2,3,4,5};
-struct Sc sc2 = {1,{2,3},4};
+struct Sc sc2 = {1,{2,3},4};
struct Sc sc3 = {1,2,3,4};
struct Sc sq0 = {2,{2,2},2};
@@ -73,3 +73,28 @@ void main (int a){return;};
requires qed_ko: indirect_init_union_t: u.t[0] == 0;
*/
void main_ko (void){return;}
+
+const int ta1[5] = { [2]=1,[4]=1 };
+/*@ ensures qed_ok: ta1[0]==ta1[1] && ta1[1]==ta1[3];
+ @ ensures qed_ko: ta1[4]==0;
+ @ ensures qed_ko: ta1[3]==1; */
+void fa1(void) {return ;}
+
+const int ta2[5] = { [2 ... 3]=1 };
+/*@ ensures qed_ok: ta2[0]==ta2[1] && ta2[1]==ta2[4];
+ @ ensures qed_ko: ta2[4]==1;
+ @ ensures qed_ko: ta2[1]==1; */
+void fa2(void) {return ;}
+
+const int ta3[5] = { [1]=1, [3]=1};
+/*@ ensures qed_ok: ta3[0]==ta3[2] && ta1[2]==ta1[4];
+ @ ensures qed_ko: ta3[0]==1;
+ @ ensures qed_ko: ta3[2]==1;
+ @ ensures qed_ko: ta2[4]==1; */
+void fa3(void) {return ;}
+
+const struct { int a, b, c; } ts1[4] = { [2].a=1, [2].b=1 };
+/*@ ensures qed_ok: ts1[0]==ts1[1] && ts1[1]==ts1[3] && ts1[2].a ==ts1[2].b;
+ @ ensures qed_ko: ts1[2].c==1;
+ @ ensures qed_ko: ts1[0].a==1;*/
+void fs1(void) {return ;}
diff --git a/src/plugins/wp/tests/wp_acsl/init_value.i.0.report.json b/src/plugins/wp/tests/wp_acsl/init_value.i.0.report.json
index 98c5b78ddb0..ed3d6417287 100644
--- a/src/plugins/wp/tests/wp_acsl/init_value.i.0.report.json
+++ b/src/plugins/wp/tests/wp_acsl/init_value.i.0.report.json
@@ -1,6 +1,6 @@
-{ "wp:global": { "alt-ergo": { "total": 6, "valid": 6, "rank": 8 },
- "qed": { "total": 14, "valid": 14 },
- "wp:main": { "total": 20, "valid": 20, "rank": 8 } },
+{ "wp:global": { "alt-ergo": { "total": 7, "valid": 7, "rank": 29 },
+ "qed": { "total": 17, "valid": 17 },
+ "wp:main": { "total": 24, "valid": 24, "rank": 29 } },
"wp:functions": { "main": { "main_pre_qed_ok_direct_init_union": { "qed":
{ "total": 1,
"valid": 1 },
@@ -116,4 +116,40 @@
"valid": 14 },
"wp:main": { "total": 20,
"valid": 20,
- "rank": 8 } } } } }
+ "rank": 8 } } },
+ "fa1": { "fa1_post_qed_ok": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "fa2": { "fa2_post_qed_ok": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "fa3": { "fa3_post_qed_ok": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "fs1": { "fs1_post_qed_ok": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 29 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 29 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 29 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 29 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/init_value.i.1.report.json b/src/plugins/wp/tests/wp_acsl/init_value.i.1.report.json
index 25df975e11a..a90fa9753d4 100644
--- a/src/plugins/wp/tests/wp_acsl/init_value.i.1.report.json
+++ b/src/plugins/wp/tests/wp_acsl/init_value.i.1.report.json
@@ -1,5 +1,5 @@
-{ "wp:global": { "alt-ergo": { "total": 9, "unknown": 9 },
- "wp:main": { "total": 9, "unknown": 9 } },
+{ "wp:global": { "alt-ergo": { "total": 18, "unknown": 18 },
+ "wp:main": { "total": 18, "unknown": 18 } },
"wp:functions": { "main_ko": { "main_ko_pre_qed_ko_indirect_init_union_t":
{ "alt-ergo": { "total": 1, "unknown": 1 },
"wp:main": { "total": 1, "unknown": 1 } },
@@ -45,4 +45,56 @@
"wp:section": { "alt-ergo": { "total": 9,
"unknown": 9 },
"wp:main": { "total": 9,
- "unknown": 9 } } } } }
+ "unknown": 9 } } },
+ "fa1": { "fa1_post_qed_ko_2": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "fa1_post_qed_ko": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } } },
+ "fa2": { "fa2_post_qed_ko_2": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "fa2_post_qed_ko": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } } },
+ "fa3": { "fa3_post_qed_ko_3": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "fa3_post_qed_ko_2": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "fa3_post_qed_ko": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 3,
+ "unknown": 3 },
+ "wp:main": { "total": 3,
+ "unknown": 3 } } },
+ "fs1": { "fs1_post_qed_ko_2": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "fs1_post_qed_ko": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
index 3c3248ae43b..bcd9a305a13 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
@@ -3,6 +3,287 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function fa1
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ok' in 'fa1':
+Let x = ta1_0[4].
+Let x_1 = ta1_0[0].
+Let x_2 = ta1_0[1].
+Let x_3 = ta1_0[3].
+Assume {
+ Type: is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\ is_sint32(x).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
+ (* Initializer *)
+ Init: ta1_0[2] = 1.
+ (* Initializer *)
+ Init: x = 1.
+ (* Initializer *)
+ Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
+}
+Prove: (x_2 = x_1) /\ (x_3 = x_2).
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa1':
+Let x = ta1_0[4].
+Assume {
+ Type: is_sint32(ta1_0[0]) /\ is_sint32(ta1_0[1]) /\ is_sint32(ta1_0[3]) /\
+ is_sint32(x).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
+ (* Initializer *)
+ Init: ta1_0[2] = 1.
+ (* Initializer *)
+ Init: x = 1.
+ (* Initializer *)
+ Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa1':
+Let x = ta1_0[4].
+Let x_1 = ta1_0[3].
+Assume {
+ Type: is_sint32(ta1_0[0]) /\ is_sint32(ta1_0[1]) /\ is_sint32(x_1) /\
+ is_sint32(x).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
+ (* Initializer *)
+ Init: ta1_0[2] = 1.
+ (* Initializer *)
+ Init: x = 1.
+ (* Initializer *)
+ Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
+}
+Prove: x_1 = 1.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fa2
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ok' in 'fa2':
+Let x = ta2_0[0].
+Let x_1 = ta2_0[1].
+Let x_2 = ta2_0[4].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta2_0[i] = 0))).
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 3) -> (ta2_0[i] = 1))).
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta2_0[i] = 0))).
+}
+Prove: (x_1 = x) /\ (x_2 = x_1).
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa2':
+Let x = ta2_0[4].
+Assume {
+ Type: is_sint32(ta2_0[0]) /\ is_sint32(ta2_0[1]) /\ is_sint32(x).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta2_0[i] = 0))).
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 3) -> (ta2_0[i] = 1))).
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta2_0[i] = 0))).
+}
+Prove: x = 1.
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa2':
+Let x = ta2_0[1].
+Assume {
+ Type: is_sint32(ta2_0[0]) /\ is_sint32(x) /\ is_sint32(ta2_0[4]).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta2_0[i] = 0))).
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 3) -> (ta2_0[i] = 1))).
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta2_0[i] = 0))).
+}
+Prove: x = 1.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fa3
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ok' in 'fa3':
+Let x = ta1_0[4].
+Let x_1 = ta1_0[2].
+Let x_2 = ta3_0[0].
+Let x_3 = ta3_0[2].
+Assume {
+ Type: is_sint32(x_1) /\ is_sint32(x) /\ is_sint32(x_2) /\ is_sint32(x_3).
+ (* Initializer *)
+ Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
+ (* Initializer *)
+ Init: ta3_0[1] = 1.
+ (* Initializer *)
+ Init: ta3_0[3] = 1.
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (ta3_0[i] = 0))).
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta3_0[i] = 0))).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
+ (* Initializer *)
+ Init: x_1 = 1.
+ (* Initializer *)
+ Init: x = 1.
+ (* Initializer *)
+ Init: forall i : Z. ((3 <= i) -> ((i <= 3) -> (ta1_0[i] = 0))).
+}
+Prove: (x = x_1) /\ (x_3 = x_2).
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa3':
+Let x = ta3_0[0].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(ta3_0[2]).
+ (* Initializer *)
+ Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
+ (* Initializer *)
+ Init: ta3_0[1] = 1.
+ (* Initializer *)
+ Init: ta3_0[3] = 1.
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (ta3_0[i] = 0))).
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta3_0[i] = 0))).
+}
+Prove: x = 1.
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa3':
+Let x = ta3_0[2].
+Assume {
+ Type: is_sint32(ta3_0[0]) /\ is_sint32(x).
+ (* Initializer *)
+ Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
+ (* Initializer *)
+ Init: ta3_0[1] = 1.
+ (* Initializer *)
+ Init: ta3_0[3] = 1.
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (ta3_0[i] = 0))).
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta3_0[i] = 0))).
+}
+Prove: x = 1.
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa3':
+Let x = ta2_0[4].
+Assume {
+ Type: is_sint32(x).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta2_0[i] = 0))).
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 3) -> (ta2_0[i] = 1))).
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (ta2_0[i] = 0))).
+}
+Prove: x = 1.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fs1
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ok' in 'fs1':
+Let a = ts1_0[2].
+Let x = a.F5_c.
+Let x_1 = a.F5_b.
+Let x_2 = a.F5_a.
+Let a_1 = ts1_0[0].
+Let a_2 = ts1_0[1].
+Let a_3 = ts1_0[3].
+Assume {
+ Type: IsS5(a_1) /\ IsS5(a_2) /\ IsS5(a_3) /\ is_sint32(a_1.F5_a) /\
+ is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(x).
+ (* Initializer *)
+ Init: forall i : Z. let a_4 = ts1_0[i] in ((0 <= i) -> ((i <= 1) ->
+ (((a_4.F5_a) = 0) /\ ((a_4.F5_b) = 0) /\ ((a_4.F5_c) = 0)))).
+ (* Initializer *)
+ Init: x_2 = 1.
+ (* Initializer *)
+ Init: x_1 = 1.
+ (* Initializer *)
+ Init: x = 0.
+ (* Initializer *)
+ Init: forall i : Z. let a_4 = ts1_0[i] in ((3 <= i) -> ((i <= 3) ->
+ (((a_4.F5_a) = 0) /\ ((a_4.F5_b) = 0) /\ ((a_4.F5_c) = 0)))).
+}
+Prove: (x_1 = x_2) /\ EqS5(a_1, a_2) /\ EqS5(a_2, a_3).
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fs1':
+Let a = ts1_0[2].
+Let x = a.F5_c.
+Let x_1 = a.F5_b.
+Let x_2 = a.F5_a.
+Let a_1 = ts1_0[0].
+Assume {
+ Type: IsS5(a_1) /\ IsS5(ts1_0[1]) /\ IsS5(ts1_0[3]) /\
+ is_sint32(a_1.F5_a) /\ is_sint32(x_2) /\ is_sint32(x_1) /\
+ is_sint32(x).
+ (* Initializer *)
+ Init: forall i : Z. let a_2 = ts1_0[i] in ((0 <= i) -> ((i <= 1) ->
+ (((a_2.F5_a) = 0) /\ ((a_2.F5_b) = 0) /\ ((a_2.F5_c) = 0)))).
+ (* Initializer *)
+ Init: x_2 = 1.
+ (* Initializer *)
+ Init: x_1 = 1.
+ (* Initializer *)
+ Init: x = 0.
+ (* Initializer *)
+ Init: forall i : Z. let a_2 = ts1_0[i] in ((3 <= i) -> ((i <= 3) ->
+ (((a_2.F5_a) = 0) /\ ((a_2.F5_b) = 0) /\ ((a_2.F5_c) = 0)))).
+}
+Prove: x = 1.
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fs1':
+Let a = ts1_0[2].
+Let x = a.F5_c.
+Let x_1 = a.F5_b.
+Let x_2 = a.F5_a.
+Let a_1 = ts1_0[0].
+Let x_3 = a_1.F5_a.
+Assume {
+ Type: IsS5(a_1) /\ IsS5(ts1_0[1]) /\ IsS5(ts1_0[3]) /\ is_sint32(x_3) /\
+ is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(x).
+ (* Initializer *)
+ Init: forall i : Z. let a_2 = ts1_0[i] in ((0 <= i) -> ((i <= 1) ->
+ (((a_2.F5_a) = 0) /\ ((a_2.F5_b) = 0) /\ ((a_2.F5_c) = 0)))).
+ (* Initializer *)
+ Init: x_2 = 1.
+ (* Initializer *)
+ Init: x_1 = 1.
+ (* Initializer *)
+ Init: x = 0.
+ (* Initializer *)
+ Init: forall i : Z. let a_2 = ts1_0[i] in ((3 <= i) -> ((i <= 3) ->
+ (((a_2.F5_a) = 0) /\ ((a_2.F5_b) = 0) /\ ((a_2.F5_c) = 0)))).
+}
+Prove: x_3 = 1.
+
+------------------------------------------------------------
------------------------------------------------------------
Function main
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
index 550a8ff60c4..125cf6eebc1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
@@ -3,6 +3,142 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function fa1
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ok' in 'fa1':
+Let x = ta1_0[0].
+Let x_1 = ta1_0[1].
+Let x_2 = ta1_0[3].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\
+ is_sint32(ta1_0[4]).
+}
+Prove: (x_1 = x) /\ (x_2 = x_1).
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa1':
+Let x = ta1_0[4].
+Assume {
+ Type: is_sint32(ta1_0[0]) /\ is_sint32(ta1_0[1]) /\ is_sint32(ta1_0[3]) /\
+ is_sint32(x).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa1':
+Let x = ta1_0[3].
+Assume {
+ Type: is_sint32(ta1_0[0]) /\ is_sint32(ta1_0[1]) /\ is_sint32(x) /\
+ is_sint32(ta1_0[4]).
+}
+Prove: x = 1.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fa2
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ok' in 'fa2':
+Let x = ta2_0[0].
+Let x_1 = ta2_0[1].
+Let x_2 = ta2_0[4].
+Assume { Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2). }
+Prove: (x_1 = x) /\ (x_2 = x_1).
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa2':
+Let x = ta2_0[4].
+Assume { Type: is_sint32(ta2_0[0]) /\ is_sint32(ta2_0[1]) /\ is_sint32(x). }
+Prove: x = 1.
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa2':
+Let x = ta2_0[1].
+Assume { Type: is_sint32(ta2_0[0]) /\ is_sint32(x) /\ is_sint32(ta2_0[4]). }
+Prove: x = 1.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fa3
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ok' in 'fa3':
+Let x = ta1_0[2].
+Let x_1 = ta1_0[4].
+Let x_2 = ta3_0[0].
+Let x_3 = ta3_0[2].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3).
+}
+Prove: (x_1 = x) /\ (x_3 = x_2).
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa3':
+Let x = ta3_0[0]. Assume { Type: is_sint32(x) /\ is_sint32(ta3_0[2]). }
+Prove: x = 1.
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa3':
+Let x = ta3_0[2]. Assume { Type: is_sint32(ta3_0[0]) /\ is_sint32(x). }
+Prove: x = 1.
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fa3':
+Let x = ta2_0[4]. Assume { Type: is_sint32(x). }
+Prove: x = 1.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fs1
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ok' in 'fs1':
+Let a = ts1_0[0].
+Let a_1 = ts1_0[1].
+Let a_2 = ts1_0[3].
+Let a_3 = ts1_0[2].
+Let x = a_3.F5_a.
+Let x_1 = a_3.F5_b.
+Assume {
+ Type: IsS5(a) /\ IsS5(a_1) /\ IsS5(a_2) /\ is_sint32(a.F5_a) /\
+ is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(a_3.F5_c).
+}
+Prove: (x_1 = x) /\ EqS5(a, a_1) /\ EqS5(a_1, a_2).
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fs1':
+Let a = ts1_0[0].
+Let a_1 = ts1_0[2].
+Let x = a_1.F5_c.
+Assume {
+ Type: IsS5(a) /\ IsS5(ts1_0[1]) /\ IsS5(ts1_0[3]) /\ is_sint32(a.F5_a) /\
+ is_sint32(a_1.F5_a) /\ is_sint32(a_1.F5_b) /\ is_sint32(x).
+}
+Prove: x = 1.
+
+------------------------------------------------------------
+
+Goal Post-condition 'qed_ko' in 'fs1':
+Let a = ts1_0[0].
+Let x = a.F5_a.
+Let a_1 = ts1_0[2].
+Assume {
+ Type: IsS5(a) /\ IsS5(ts1_0[1]) /\ IsS5(ts1_0[3]) /\ is_sint32(x) /\
+ is_sint32(a_1.F5_a) /\ is_sint32(a_1.F5_b) /\ is_sint32(a_1.F5_c).
+}
+Prove: x = 1.
+
+------------------------------------------------------------
------------------------------------------------------------
Function main_ko
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
index 047f9288faf..83fb6692169 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
@@ -3,7 +3,11 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 20 goals scheduled
+[wp] 24 goals scheduled
+[wp] [Qed] Goal typed_fa1_post_qed_ok : Valid
+[wp] [Qed] Goal typed_fa2_post_qed_ok : Valid
+[wp] [Qed] Goal typed_fa3_post_qed_ok : Valid
+[wp] [Alt-Ergo] Goal typed_fs1_post_qed_ok : Valid
[wp] [Qed] Goal typed_main_pre_qed_ok_Struct_Simple_a : Valid
[wp] [Qed] Goal typed_main_pre_qed_ok_Struct_Simple_b : Valid
[wp] [Qed] Goal typed_main_pre_qed_ok_Simple_Array_0 : Valid
@@ -24,11 +28,15 @@
[wp] [Alt-Ergo] Goal typed_main_pre_qed_ok_4 : Valid
[wp] [Alt-Ergo] Goal typed_main_pre_qed_ok_5 : Valid
[wp] [Qed] Goal typed_main_pre_qed_ok_direct_init_union : Valid
-[wp] Proved goals: 20 / 20
- Qed: 14
- Alt-Ergo: 6
+[wp] Proved goals: 24 / 24
+ Qed: 17
+ Alt-Ergo: 7
[wp] Report 'tests/wp_acsl/init_value.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
main 14 6 (28..40) 20 100%
+fa1 1 - 1 100%
+fa2 1 - 1 100%
+fa3 1 - 1 100%
+fs1 - 1 (160..184) 1 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
index d33e3e1ce3b..d779e53743f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
@@ -3,7 +3,16 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 9 goals scheduled
+[wp] 18 goals scheduled
+[wp] [Alt-Ergo] Goal typed_fa1_post_qed_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_fa1_post_qed_ko_2 : Unknown
+[wp] [Alt-Ergo] Goal typed_fa2_post_qed_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_fa2_post_qed_ko_2 : Unknown
+[wp] [Alt-Ergo] Goal typed_fa3_post_qed_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_fa3_post_qed_ko_2 : Unknown
+[wp] [Alt-Ergo] Goal typed_fa3_post_qed_ko_3 : Unknown
+[wp] [Alt-Ergo] Goal typed_fs1_post_qed_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_fs1_post_qed_ko_2 : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_pre_qed_ko_Sc_eq_ko : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_pre_qed_ko_Sc_t : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_pre_qed_ko_Sc_c_2 : Unknown
@@ -13,10 +22,14 @@
[wp] [Alt-Ergo] Goal typed_main_ko_pre_qed_ko_T1_6 : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_pre_qed_ko_indirect_init_union_b : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_pre_qed_ko_indirect_init_union_t : Unknown
-[wp] Proved goals: 0 / 9
- Alt-Ergo: 0 (unknown: 9)
+[wp] Proved goals: 0 / 18
+ Alt-Ergo: 0 (unknown: 18)
[wp] Report 'tests/wp_acsl/init_value.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
main_ko - - 9 0.0%
+fa1 - - 2 0.0%
+fa2 - - 2 0.0%
+fa3 - - 3 0.0%
+fs1 - - 2 0.0%
-------------------------------------------------------------
--
GitLab