diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
index d7c91e8c587cda072659f627edf1409be880ede6..d1946539852b596ec8eb961d2858433278d7c44e 100644
--- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
@@ -352,7 +352,7 @@ new way
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
- Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
+ Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
@@ -370,7 +370,7 @@ Prove: foo_0 = 1.
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
- Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
+ Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
@@ -387,7 +387,7 @@ Prove: true.
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
- Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
+ Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
@@ -405,8 +405,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i_1 = 0.
+ Have: (ta_i_0=true) /\ (ta_i_1=false).
+ Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i <= 10.
@@ -428,8 +428,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i = 0.
+ Have: (ta_i_0=true) /\ (ta_i_1=false).
+ Have: (Init_i_0=true) /\ (i = 0).
Have: (Init_i_1=true) /\ ((1 + i) = i_1).
Have: i_1 <= 10.
Have: i_2 <= 10.
@@ -448,8 +448,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i_1 = 0.
+ Have: (ta_i_0=true) /\ (ta_i_1=false).
+ Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i <= 10.
@@ -467,8 +467,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i_1 = 0.
+ Have: (ta_i_0=true) /\ (ta_i_1=false).
+ Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i <= 10.
@@ -485,8 +485,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i_1 = 0.
+ Have: (ta_i_0=true) /\ (ta_i_1=false).
+ Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i).
}
Prove: i <= 10.
@@ -500,8 +500,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i_1 = 0.
+ Have: (ta_i_0=true) /\ (ta_i_1=false).
+ Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i_3 <= 10.
@@ -520,8 +520,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i = 0.
+ Have: (ta_i_0=true) /\ (ta_i_1=false).
+ Have: (Init_i_0=true) /\ (i = 0).
Have: (Init_i_1=true) /\ ((1 + i) = i_1).
Have: i_1 <= 10.
Have: i_2 <= 10.
diff --git a/src/plugins/wp/tests/wp_acsl/initialized_local_init.i b/src/plugins/wp/tests/wp_acsl/initialized_local_init.i
new file mode 100644
index 0000000000000000000000000000000000000000..3fe1467bc0fc358b7ca5ad95a300ae2e3d4971d3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/initialized_local_init.i
@@ -0,0 +1,19 @@
+void l_int(void){
+ int x = 1 ;
+ //@ assert SUCCS: x == 1;
+ //@ assert SUCCS: \initialized(&x);
+ //@ check FAILS: \false ;
+}
+void l_array(void){
+ int x[3] = { 0 } ;
+ //@ assert SUCCS: x[0] == x[1] == x[2] == 0 ;
+ //@ assert SUCCS: \initialized(&x);
+ //@ check FAILS: \false ;
+}
+typedef struct { int x ; char t[2] ; } S;
+void l_struct(void){
+ S s = { 0 };
+ //@ assert SUCCS: s.x == s.t[0] == s.t[1] == 0 ;
+ //@ assert SUCCS: \initialized(&s);
+ //@ check FAILS: \false ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_local_init.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_local_init.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b64e2acc93c3758f0b4fd6bc7bdcec4280dd0cbe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_local_init.res.oracle
@@ -0,0 +1,89 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_local_init.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function l_array
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 9):
+Let x_1 = x[1].
+Let x_2 = x[2].
+Assume {
+ Type: is_sint32(x_1) /\ is_sint32(x_2).
+ (* Initializer *)
+ Init: x[0] = 0.
+ (* Initializer *)
+ Init: forall i : Z. ((0 < i) -> ((i <= 2) -> (x[i] = 0))).
+}
+Prove: (x_1 = 0) /\ (x_2 = 0) /\ (x_2 = x_1).
+
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 10):
+Assume {
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 2).
+ (* Initializer *)
+ Init: (Init_x_0[0]=true).
+ (* Initializer *)
+ Init: x[0] = 0.
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) -> (Init_x_0[i_1]=true))).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) -> (x[i_1] = 0))).
+ (* Assertion 'SUCCS' *)
+ Have: (x[1] = 0) /\ (x[2] = 0).
+}
+Prove: (Init_x_0[i]=true).
+
+------------------------------------------------------------
+
+Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 11):
+Assume {
+ (* Initializer *)
+ Init: x[0] = 0.
+ (* Initializer *)
+ Init: forall i : Z. ((0 < i) -> ((i <= 2) -> (x[i] = 0))).
+ (* Assertion 'SUCCS' *)
+ Have: (x[1] = 0) /\ (x[2] = 0).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function l_int
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 4):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 5):
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function l_struct
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 17):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 18):
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index 0a7a16a6acadb3ef41857bbbff863c300b5da1be..083f7d0ff4956ba090210e61d5f4da2817ea3822 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -251,9 +251,6 @@ Assume {
is_sint8_chunk(Mchar_0).
Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
- (* Block In *)
- Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
- Init_r_0.
}
Prove: valid_rd(Malloc_0, p, 3).
@@ -273,9 +270,6 @@ Assume {
is_sint8_chunk(Mchar_0).
Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
- (* Block In *)
- Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
- Init_r_0.
(* Assertion 'rte,mem_access' *)
Have: valid_rd(Malloc_0, p, 3).
(* Initializer *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_local_init.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_local_init.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..59f14e4c07355254a07c778ce5667226b7dcb2f1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_local_init.res.oracle
@@ -0,0 +1,23 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_local_init.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 9 goals scheduled
+[wp] [Qed] Goal typed_l_int_assert_SUCCS : Valid
+[wp] [Qed] Goal typed_l_int_assert_SUCCS_2 : Valid
+[wp] [Alt-Ergo] Goal typed_l_int_check_FAILS : Unsuccess
+[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS : Valid (missing cache)
+[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS_2 : Valid (missing cache)
+[wp] [Alt-Ergo] Goal typed_l_array_check_FAILS : Unsuccess
+[wp] [Qed] Goal typed_l_struct_assert_SUCCS : Valid
+[wp] [Qed] Goal typed_l_struct_assert_SUCCS_2 : Valid
+[wp] [Alt-Ergo] Goal typed_l_struct_check_FAILS : Unsuccess
+[wp] Proved goals: 6 / 9
+ Qed: 4
+ Alt-Ergo: 2 (unsuccess: 3)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ l_int 2 - 3 66.7%
+ l_array - 2 3 66.7%
+ l_struct 2 - 3 66.7%
+------------------------------------------------------------