diff --git a/src/plugins/wp/CodeSemantics.ml b/src/plugins/wp/CodeSemantics.ml
index e7dacab67bf5ee7a8fb910ca905891cea21f3ce2..d1c55685ea4d7add16b3f3e43080df932afe60c3 100644
--- a/src/plugins/wp/CodeSemantics.ml
+++ b/src/plugins/wp/CodeSemantics.ml
@@ -32,6 +32,26 @@ open Sigs
open Lang
open Lang.F
+module WpLog = Wp_parameters
+let constfold_ctyp = function
+ | TArray (_,Some {enode = (Const CInt64 _) },_,_) as ct -> ct
+ | TArray (ty,Some len,cache,attr) as ct -> begin
+ match Cil.constFold true len with
+ | {enode = (Const CInt64 _) } as len ->
+ TArray(ty,Some len,cache,attr)
+ | _ -> ct
+ end
+ | ct -> ct
+
+let constfold_coffset = function
+ | Index({enode=Const (CInt64 _)}, _) as off -> off
+ | Index(idx, next) as off -> begin
+ match Cil.constFold true idx with
+ | {enode = (Const CInt64 _) } as idx -> Index(idx, next)
+ | _ -> off
+ end
+ | off -> off
+
module Make(M : Sigs.Model) =
struct
@@ -448,22 +468,18 @@ struct
init_value ~sigma lv (Cil.typeOfLval lv) (Some exp) :: acc
| CompoundInit ( ct , initl ) ->
-
- let len = List.length initl in
- let acc =
+ let ct = constfold_ctyp ct in
+ let acc = (* updated acc with default init of structure *)
match ct with
- | TArray (ty,Some {enode = (Const CInt64 (size,_,_))},_,_)
- when Integer.lt (Integer.of_int len) size ->
- init_range ~sigma lv ty (Integer.of_int len) size None :: acc
-
- | TComp (cp,_,_) when len < (List.length cp.cfields) ->
-
+ | TComp (cp,_,_) when cp.cstruct && (* not for union... *)
+ (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
@@ -477,47 +493,80 @@ struct
| _ -> acc
in
match ct with
- | TArray (ty,_,_,_)
- when Wp_parameters.InitWithForall.get () ->
- (* 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
- *)
+ | TArray (ty,len,_,_) ->
+ let delayed =
+ match len with (* number of required elements *)
+ | Some {enode = (Const CInt64 (size,_,_))} ->
+ (size, None)
+ | _ -> (* CIL invariant broken. *)
+ WpLog.fatal "CIL invariant broken: unknown initialized array size"
+ in
let make_quant acc = function
- | None -> acc
- | Some (Index({enode=Const (CInt64 (i0,_,_))}, NoOffset),exp,il)
- when Integer.lt il i0 ->
+ (* adds delayed initializations from info about
+ the last consecutive indices having
+ the same value, but that have not yet initialized. *)
+ | (_,None) -> acc (* nothing was delayed *)
+ | (il,Some (i0,_,exp)) when Integer.lt il i0 ->
+ (* Added pred: \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,_) ->
+ | (_il,Some (_i0,off,exp)) ->
+ (* case [_il=_i0], so uses [off] corresponding to [_i0]
+ Added pred: t[i]==exp*)
let lv = Cil.addOffsetLval off lv in
init_value ~sigma lv ty (Some exp) :: acc
in
+ let add_missing_indices acc i0 = function
+ (* adds eventual default value for missing indices. *)
+ | (i1, _) ->
+ if Integer.ge i0 i1 then (* no hole *) acc
+ else (* defaults values
+ Added pred: \forall i \in [i0 .. i1[ ; t[i]==default *)
+ init_range ~sigma lv ty i0 i1 None :: acc
+ in
let acc, delayed =
List.fold_left
(fun (acc,delayed) (off,init) ->
- match delayed, off, init with
- | None, Index({enode=Const (CInt64 (i0,_,_))}, NoOffset),
- SingleInit curr ->
- (acc,Some(off,curr,i0))
- | Some (i0,prev,ip), Index({enode=Const (CInt64 (i,_,_))}, NoOffset),
- SingleInit curr
- when ExpStructEq.equal prev curr
- && Integer.equal (Integer.pred ip) i ->
- (acc,Some(i0,prev,i))
- | _, _,_ ->
+ let off = constfold_coffset off in
+ let idx,acc = match off with
+ | Index({enode=Const CInt64 (idx,_,_)}, _) ->
+ (match delayed with
+ | (iprev, _) when Integer.lt iprev idx ->
+ (* CIL invariant broken.
+ without that invariant, an algo with a 2sd pass
+ is required for introducing default values *)
+ WpLog.fatal "CIL invariant broken: unordered initializer";
+ | _ -> ()) ;
+ idx,
+ (* adds default values for missing indices *)
+ add_missing_indices acc (Integer.succ idx) delayed
+ | _ -> (* CIL invariant broken. *)
+ WpLog.fatal "CIL invariant broken: unknown initialized index"
+ in
+ match off, init with (* only simple init can be delayed *)
+ | Index(_, NoOffset), SingleInit init -> begin
+ match delayed with
+ | (i_prev,(Some (_,_,init_delayed) as delayed_info))
+ when Wp_parameters.InitWithForall.get ()
+ && Integer.equal (Integer.pred i_prev) idx
+ && ExpStructEq.equal init_delayed init ->
+ acc, (idx,delayed_info)
+ | _ -> (* flush the delayed init, and store the new one *)
+ let acc = make_quant acc delayed in
+ acc, (idx, Some (idx,off,init))
+ end
+ | Index(_, _),_ ->
+ (* flush the delayed init, and adds the current one *)
let acc = make_quant acc delayed in
- begin match off, init with
- | Index({enode=Const (CInt64 (i0,_,_))}, NoOffset),
- SingleInit curr ->
- acc, Some (off,curr,i0)
- | _ ->
- let lv = Cil.addOffsetLval off lv in
- init_variable ~sigma lv init acc, None
- end)
- (acc,None)
- (List.rev initl) in
- (make_quant acc delayed)
+ let lv = Cil.addOffsetLval off lv in
+ (init_variable ~sigma lv init acc), (idx, None)
+ | _ -> WpLog.fatal "CIL invariant broken: not an index"
+ )
+ (acc,delayed)
+ (List.rev initl)
+ in
+ let acc = make_quant acc delayed in
+ 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 382ae866678afdd2183fd0ef54a7f9a2e88625e0..b9d9caeabadd4510e4a64607a265906f70f4274c 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:
- OPT: -main main_ko
+ 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
*/
@@ -11,25 +11,33 @@
/* --- GOAL: partial and complete initialization of value --- */
/* -------------------------------------------------------------------------- */
-struct S { int a; int b;};
+struct S { int a; int b;};
struct S s = {2};
int t[2] = {1};
+int t1[9+1] = {[5 ... 6]=2, [0 ... 3 ]=1 };
-struct St {int tab[10];};
+struct St {int tab[9+1];};
struct St st = {{1,2,3,4}};
-struct Sc {int a; int b[3]; int c;};
+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};
+struct Sc sq1 = {.b={2,2}};
+
unsigned char tab[32];
-int u [];
+union U {
+ short t[4];
+ short a;
+ long long b;
+} u = {.a=-1 };
/*@ requires qed_ok: Struct_Simple_a: s.a == 2 ;
requires qed_ok: Struct_Simple_b: s.b == 0 ;
@@ -44,8 +52,15 @@ int u [];
requires qed_ok: Sc_c_3 : sc3.c == 0;
requires qed_ok: Tab_no_init : tab[5] == 0 ;
requires qed_ok: Tab_todo : \forall int i; 0 <= i <= 31 ==> tab[i] <= 255;
+ requires qed_ok: sq0.b[1]==2;
+ requires qed_ok: sq0.b[2]==0;
+ requires qed_ok: \forall integer i; 0 <= i <= 3 ==> t1[i] == 1;
+ requires qed_ok: todo: t1[4] == 0;
+ requires qed_ok: \forall integer i; 5 < i <= 6 ==> t1[i] == 2;
+ requires qed_ok: \forall integer i; 6 < i <= 9 ==> t1[i] == 0;
+ requires qed_ok: direct_init_union: u.a == -1;
*/
-void main (void){return;}
+void main (int a){return;};
/*@ requires qed_ko: Sc_eq_ko : sc2 == sc3;
requires qed_ko: Sc_t : sc3.b[2] == 3 ;
@@ -53,6 +68,33 @@ void main (void){return;}
requires qed_ko: Tab_no_init : tab[5] == 1 ;
requires qed_ko: With_Array_Struct_3 : st.tab[3] == 3 ;
requires qed_ko: Simple_Array_1 : t[1] == 1 ;
+ requires qed_ko: T1_6: t1[6] == 0;
+ requires qed_ko: indirect_init_union_b: u.b == 0;
+ 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 24349b32c01b0a4eff5f6e5927b4825c7cf3f059..ed3d641728778606547731d1d152cd81ce12ddbd 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,7 +1,43 @@
-{ "wp:global": { "alt-ergo": { "total": 3, "valid": 3, "rank": 8 },
- "qed": { "total": 10, "valid": 10 },
- "wp:main": { "total": 13, "valid": 13, "rank": 8 } },
- "wp:functions": { "main": { "main_pre_qed_ok_Tab_todo": { "alt-ergo":
+{ "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 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "main_pre_qed_ok_5": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } },
+ "main_pre_qed_ok_4": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } },
+ "main_pre_qed_ok_todo": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "main_pre_qed_ok_3": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } },
+ "main_pre_qed_ok_2": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "main_pre_qed_ok": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "main_pre_qed_ok_Tab_todo": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 2 },
@@ -73,11 +109,47 @@
"wp:main":
{ "total": 1,
"valid": 1 } },
- "wp:section": { "alt-ergo": { "total": 3,
- "valid": 3,
+ "wp:section": { "alt-ergo": { "total": 6,
+ "valid": 6,
"rank": 8 },
- "qed": { "total": 10,
- "valid": 10 },
- "wp:main": { "total": 13,
- "valid": 13,
- "rank": 8 } } } } }
+ "qed": { "total": 14,
+ "valid": 14 },
+ "wp:main": { "total": 20,
+ "valid": 20,
+ "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 7c26ecf79edec8169bee2869e3b2fa07bb08e876..a90fa9753d457fe09ba9c0a8dc032f363b91a00e 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,6 +1,18 @@
-{ "wp:global": { "alt-ergo": { "total": 6, "unknown": 6 },
- "wp:main": { "total": 6, "unknown": 6 } },
- "wp:functions": { "main_ko": { "main_ko_pre_qed_ko_Simple_Array_1":
+{ "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 } },
+ "main_ko_pre_qed_ko_indirect_init_union_b":
+ { "alt-ergo": { "total": 1, "unknown": 1 },
+ "wp:main": { "total": 1, "unknown": 1 } },
+ "main_ko_pre_qed_ko_T1_6": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_ko_pre_qed_ko_Simple_Array_1":
{ "alt-ergo": { "total": 1, "unknown": 1 },
"wp:main": { "total": 1, "unknown": 1 } },
"main_ko_pre_qed_ko_With_Array_Struct_3":
@@ -30,7 +42,59 @@
"wp:main":
{ "total": 1,
"unknown": 1 } },
- "wp:section": { "alt-ergo": { "total": 6,
- "unknown": 6 },
- "wp:main": { "total": 6,
- "unknown": 6 } } } } }
+ "wp:section": { "alt-ergo": { "total": 9,
+ "unknown": 9 },
+ "wp:main": { "total": 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 ad4d9f1ea971d2c837da496bee9cee9a1fa814ba..bcd9a305a139c01b26fa11ccc56af7dbdfd3c080 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
@@ -1,47 +1,386 @@
-# frama-c -wp [...]
+# frama-c -wp -wp-no-let [...]
[kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing)
[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
------------------------------------------------------------
Goal Pre-condition 'qed_ok,Struct_Simple_a' in 'main':
-Prove: true.
+Let x = s.F1_S_b.
+Let x_1 = s.F1_S_a.
+Assume {
+ Type: is_sint32(x_1) /\ is_sint32(x).
+ (* Initializer *)
+ Init: x_1 = 2.
+ (* Initializer *)
+ Init: x = 0.
+}
+Prove: x_1 = 2.
------------------------------------------------------------
Goal Pre-condition 'qed_ok,Struct_Simple_b' in 'main':
-Prove: true.
+Let x = s.F1_S_b.
+Let x_1 = s.F1_S_a.
+Assume {
+ Type: is_sint32(x_1) /\ is_sint32(x).
+ (* Initializer *)
+ Init: x_1 = 2.
+ (* Initializer *)
+ Init: x = 0.
+}
+Prove: x = 0.
------------------------------------------------------------
Goal Pre-condition 'qed_ok,Simple_Array_0' in 'main':
-Prove: true.
+Let x = t[0].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(t[1]).
+ (* Initializer *)
+ Init: x = 1.
+ (* Initializer *)
+ Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
+}
+Prove: x = 1.
------------------------------------------------------------
Goal Pre-condition 'qed_ok,Simple_Array_1' in 'main':
-Let x = t[1].
+Let x = t[0].
+Let x_1 = t[1].
Assume {
- Type: is_sint32(x).
+ Type: is_sint32(x) /\ is_sint32(x_1).
(* Initializer *)
- Init: t[0] = 1.
+ Init: x = 1.
(* Initializer *)
Init: forall i : Z. ((0 < i) -> ((i <= 1) -> (t[i] = 0))).
}
-Prove: x = 0.
+Prove: x_1 = 0.
------------------------------------------------------------
Goal Pre-condition 'qed_ok,With_Array_Struct_5' in 'main':
-Prove: true.
+Let a = st_0.F2_St_tab.
+Let a_1 = a[3].
+Let a_2 = a[5].
+Assume {
+ Type: is_sint32(a_1) /\ is_sint32(a_2).
+ (* Initializer *)
+ Init: a[0] = 1.
+ (* Initializer *)
+ Init: a[1] = 2.
+ (* Initializer *)
+ Init: a[2] = 3.
+ (* Initializer *)
+ Init: a_1 = 4.
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+}
+Prove: a_2 = 0.
------------------------------------------------------------
Goal Pre-condition 'qed_ok,With_Array_Struct_3' in 'main':
-Prove: true.
+Let a = st_0.F2_St_tab.
+Let a_1 = a[3].
+Assume {
+ Type: is_sint32(a_1) /\ is_sint32(a[5]).
+ (* Initializer *)
+ Init: a[0] = 1.
+ (* Initializer *)
+ Init: a[1] = 2.
+ (* Initializer *)
+ Init: a[2] = 3.
+ (* Initializer *)
+ Init: a_1 = 4.
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+}
+Prove: a_1 = 4.
------------------------------------------------------------
@@ -76,27 +415,96 @@ Prove: EqS3_Sc(sc1_0, sc0_0).
------------------------------------------------------------
Goal Pre-condition 'qed_ok,Sc_t' in 'main':
-Prove: true.
+Let x = sc2_0.F3_Sc_c.
+Let a = sc2_0.F3_Sc_b.
+Let a_1 = a[2].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(a_1).
+ (* Initializer *)
+ Init: (sc2_0.F3_Sc_a) = 1.
+ (* Initializer *)
+ Init: a[0] = 2.
+ (* Initializer *)
+ Init: a[1] = 3.
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
+ (* Initializer *)
+ Init: x = 4.
+}
+Prove: a_1 = 0.
------------------------------------------------------------
Goal Pre-condition 'qed_ok,Sc_t' in 'main':
-Prove: true.
+Let x = sc3_0.F3_Sc_c.
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(a_1).
+ (* Initializer *)
+ Init: (sc3_0.F3_Sc_a) = 1.
+ (* Initializer *)
+ Init: a[0] = 2.
+ (* Initializer *)
+ Init: a[1] = 3.
+ (* Initializer *)
+ Init: a_1 = 4.
+ (* Initializer *)
+ Init: x = 0.
+}
+Prove: a_1 = 4.
------------------------------------------------------------
Goal Pre-condition 'qed_ok,Sc_c_2' in 'main':
-Prove: true.
+Let x = sc2_0.F3_Sc_c.
+Let a = sc2_0.F3_Sc_b.
+Assume {
+ Type: is_sint32(x) /\ is_sint32(a[2]).
+ (* Initializer *)
+ Init: (sc2_0.F3_Sc_a) = 1.
+ (* Initializer *)
+ Init: a[0] = 2.
+ (* Initializer *)
+ Init: a[1] = 3.
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
+ (* Initializer *)
+ Init: x = 4.
+}
+Prove: x = 4.
------------------------------------------------------------
Goal Pre-condition 'qed_ok,Sc_c_3' in 'main':
-Prove: true.
+Let x = sc3_0.F3_Sc_c.
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(a_1).
+ (* Initializer *)
+ Init: (sc3_0.F3_Sc_a) = 1.
+ (* Initializer *)
+ Init: a[0] = 2.
+ (* Initializer *)
+ Init: a[1] = 3.
+ (* Initializer *)
+ Init: a_1 = 4.
+ (* Initializer *)
+ Init: x = 0.
+}
+Prove: x = 0.
------------------------------------------------------------
Goal Pre-condition 'qed_ok,Tab_no_init' in 'main':
-Prove: true.
+Let x = tab_0[5].
+Assume {
+ Type: is_uint8(x).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+}
+Prove: x = 0.
------------------------------------------------------------
@@ -111,3 +519,117 @@ Assume {
Prove: tab_0[i] <= 255.
------------------------------------------------------------
+
+Goal Pre-condition 'qed_ok' in 'main':
+Let a = sq0_0.F3_Sc_b.
+Let a_1 = a[1].
+Assume {
+ Type: is_sint32(a_1) /\ is_sint32(a[2]).
+ (* Initializer *)
+ Init: (sq0_0.F3_Sc_a) = 2.
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
+ (* Initializer *)
+ Init: (sq0_0.F3_Sc_c) = 2.
+}
+Prove: a_1 = 2.
+
+------------------------------------------------------------
+
+Goal Pre-condition 'qed_ok' in 'main':
+Let a = sq0_0.F3_Sc_b.
+Let a_1 = a[2].
+Assume {
+ Type: is_sint32(a[1]) /\ is_sint32(a_1).
+ (* Initializer *)
+ Init: (sq0_0.F3_Sc_a) = 2.
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (a[i] = 2))).
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
+ (* Initializer *)
+ Init: (sq0_0.F3_Sc_c) = 2.
+}
+Prove: a_1 = 0.
+
+------------------------------------------------------------
+
+Goal Pre-condition 'qed_ok' in 'main':
+Assume {
+ Type: is_sint32(t1_0[4]).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 3).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 3) -> (t1_0[i_1] = 1))).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((5 <= i_1) -> ((i_1 <= 6) -> (t1_0[i_1] = 2))).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 4) -> (t1_0[i_1] = 0))).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((7 <= i_1) -> ((i_1 <= 9) -> (t1_0[i_1] = 0))).
+}
+Prove: t1_0[i] = 1.
+
+------------------------------------------------------------
+
+Goal Pre-condition 'qed_ok,todo' in 'main':
+Let x = t1_0[4].
+Assume {
+ Type: is_sint32(x).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+ (* Initializer *)
+ Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+ (* Initializer *)
+ Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Pre-condition 'qed_ok' in 'main':
+Assume {
+ Type: is_sint32(t1_0[4]).
+ (* Goal *)
+ When: (6 <= i) /\ (i <= 6).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 3) -> (t1_0[i_1] = 1))).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((5 <= i_1) -> ((i_1 <= 6) -> (t1_0[i_1] = 2))).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 4) -> (t1_0[i_1] = 0))).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((7 <= i_1) -> ((i_1 <= 9) -> (t1_0[i_1] = 0))).
+}
+Prove: t1_0[i] = 2.
+
+------------------------------------------------------------
+
+Goal Pre-condition 'qed_ok' in 'main':
+Assume {
+ Type: is_sint32(t1_0[4]).
+ (* Goal *)
+ When: (7 <= i) /\ (i <= 9).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 3) -> (t1_0[i_1] = 1))).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((5 <= i_1) -> ((i_1 <= 6) -> (t1_0[i_1] = 2))).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((4 <= i_1) -> ((i_1 <= 4) -> (t1_0[i_1] = 0))).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((7 <= i_1) -> ((i_1 <= 9) -> (t1_0[i_1] = 0))).
+}
+Prove: t1_0[i] = 0.
+
+------------------------------------------------------------
+
+Goal Pre-condition 'qed_ok,direct_init_union' in 'main':
+Let x = u.F4_U_a.
+Assume { Type: is_sint16(x). (* Initializer *) Init: x = (-1). }
+Prove: x = (-1).
+
+------------------------------------------------------------
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 a95fc1f3809f0317d6310d97e8de7e9b290253c0..125cf6eebc17d9a97091d3c08a58f882d44e2219 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
@@ -1,17 +1,155 @@
-# frama-c -wp [...]
+# frama-c -wp -wp-no-let [...]
[kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing)
[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
------------------------------------------------------------
Goal Pre-condition 'qed_ko,Sc_eq_ko' in 'main_ko':
+Let x = sc2_0.F3_Sc_c.
Let a = sc2_0.F3_Sc_b.
Let a_1 = sc3_0.F3_Sc_b.
+Let a_2 = a_1[2].
Assume {
- Type: IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0).
+ Type: IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ is_sint32(x) /\ is_sint32(a_2).
(* Initializer *)
Init: (sc3_0.F3_Sc_a) = 1.
(* Initializer *)
@@ -19,7 +157,7 @@ Assume {
(* Initializer *)
Init: a_1[1] = 3.
(* Initializer *)
- Init: a_1[2] = 4.
+ Init: a_2 = 4.
(* Initializer *)
Init: (sc3_0.F3_Sc_c) = 0.
(* Initializer *)
@@ -31,29 +169,80 @@ Assume {
(* Initializer *)
Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
(* Initializer *)
- Init: (sc2_0.F3_Sc_c) = 4.
+ Init: x = 4.
}
Prove: EqS3_Sc(sc2_0, sc3_0).
------------------------------------------------------------
Goal Pre-condition 'qed_ko,Sc_t' in 'main_ko':
-Prove: false.
+Let a = sc3_0.F3_Sc_b.
+Let a_1 = a[2].
+Assume {
+ Type: IsS3_Sc(sc3_0) /\ is_sint32(a_1).
+ (* Initializer *)
+ Init: (sc3_0.F3_Sc_a) = 1.
+ (* Initializer *)
+ Init: a[0] = 2.
+ (* Initializer *)
+ Init: a[1] = 3.
+ (* Initializer *)
+ Init: a_1 = 4.
+ (* Initializer *)
+ Init: (sc3_0.F3_Sc_c) = 0.
+}
+Prove: a_1 = 3.
------------------------------------------------------------
Goal Pre-condition 'qed_ko,Sc_c_2' in 'main_ko':
-Prove: false.
+Let x = sc2_0.F3_Sc_c.
+Let a = sc2_0.F3_Sc_b.
+Assume {
+ Type: IsS3_Sc(sc2_0) /\ is_sint32(x).
+ (* Initializer *)
+ Init: (sc2_0.F3_Sc_a) = 1.
+ (* Initializer *)
+ Init: a[0] = 2.
+ (* Initializer *)
+ Init: a[1] = 3.
+ (* Initializer *)
+ Init: forall i : Z. ((2 <= i) -> ((i <= 2) -> (a[i] = 0))).
+ (* Initializer *)
+ Init: x = 4.
+}
+Prove: x = 2.
------------------------------------------------------------
Goal Pre-condition 'qed_ko,Tab_no_init' in 'main_ko':
-Prove: false.
+Let x = tab_0[5].
+Assume {
+ Type: is_uint8(x).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 31) -> (tab_0[i] = 0))).
+}
+Prove: x = 1.
------------------------------------------------------------
Goal Pre-condition 'qed_ko,With_Array_Struct_3' in 'main_ko':
-Prove: false.
+Let a = st_0.F2_St_tab.
+Let a_1 = a[3].
+Assume {
+ Type: is_sint32(a_1).
+ (* Initializer *)
+ Init: a[0] = 1.
+ (* Initializer *)
+ Init: a[1] = 2.
+ (* Initializer *)
+ Init: a[2] = 3.
+ (* Initializer *)
+ Init: a_1 = 4.
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 9) -> (a[i] = 0))).
+}
+Prove: a_1 = 3.
------------------------------------------------------------
@@ -69,3 +258,42 @@ Assume {
Prove: x = 1.
------------------------------------------------------------
+
+Goal Pre-condition 'qed_ko,T1_6' in 'main_ko':
+Let x = t1_0[6].
+Assume {
+ Type: is_sint32(x).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 3) -> (t1_0[i] = 1))).
+ (* Initializer *)
+ Init: forall i : Z. ((5 <= i) -> ((i <= 6) -> (t1_0[i] = 2))).
+ (* Initializer *)
+ Init: forall i : Z. ((4 <= i) -> ((i <= 4) -> (t1_0[i] = 0))).
+ (* Initializer *)
+ Init: forall i : Z. ((7 <= i) -> ((i <= 9) -> (t1_0[i] = 0))).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Pre-condition 'qed_ko,indirect_init_union_b' in 'main_ko':
+Let x = u.F4_U_b.
+Assume {
+ Type: is_sint64(x) /\ is_sint16((u.F4_U_t)[0]).
+ (* Initializer *)
+ Init: (u.F4_U_a) = (-1).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Pre-condition 'qed_ko,indirect_init_union_t' in 'main_ko':
+Let a = (u.F4_U_t)[0].
+Assume {
+ Type: is_sint64(u.F4_U_b) /\ is_sint16(a).
+ (* Initializer *)
+ Init: (u.F4_U_a) = (-1).
+}
+Prove: a = 0.
+
+------------------------------------------------------------
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 87c51d12edc17d9360bd1aef0ebd6ccc5fa192cd..83fb66921697c443a2b99b43cf8f9ba51d5a5b81 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] 13 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
@@ -17,11 +21,22 @@
[wp] [Qed] Goal typed_main_pre_qed_ok_Sc_c_3 : Valid
[wp] [Qed] Goal typed_main_pre_qed_ok_Tab_no_init : Valid
[wp] [Alt-Ergo] Goal typed_main_pre_qed_ok_Tab_todo : Valid
-[wp] Proved goals: 13 / 13
- Qed: 10
- Alt-Ergo: 3
+[wp] [Qed] Goal typed_main_pre_qed_ok : Valid
+[wp] [Qed] Goal typed_main_pre_qed_ok_2 : Valid
+[wp] [Alt-Ergo] Goal typed_main_pre_qed_ok_3 : Valid
+[wp] [Qed] Goal typed_main_pre_qed_ok_todo : Valid
+[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: 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 10 3 (28..40) 13 100%
+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 9ca602f4ad9efda7c9c0c3e9cfc48d54109d812f..d779e53743fb22ccbdaf2a1c04e02b0489876e18 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,17 +3,33 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 6 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
[wp] [Alt-Ergo] Goal typed_main_ko_pre_qed_ko_Tab_no_init : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_pre_qed_ko_With_Array_Struct_3 : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_pre_qed_ko_Simple_Array_1 : Unknown
-[wp] Proved goals: 0 / 6
- Alt-Ergo: 0 (unknown: 6)
+[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 / 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 - - 6 0.0%
+main_ko - - 9 0.0%
+fa1 - - 2 0.0%
+fa2 - - 2 0.0%
+fa3 - - 3 0.0%
+fs1 - - 2 0.0%
-------------------------------------------------------------