[wp] oracle updates

src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle

@@ -71,29 +71,24 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 105):
-Let a = Init_s_0.Init_F1_S_a.
 Assume {
-  Have: 0 <= i.
-  Have: i <= 9.
-  Type: is_sint32(i_1) /\ is_sint32(i_2).
+  Type: is_sint32(i) /\ is_sint32(i_1).
   (* Invariant *)
-  Have: (0 <= i_1) /\ (i_1 <= 10) /\
-      (((0 < i_1) ->
-       (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
+  Have: (0 <= i) /\ (i <= 10) /\
+      (((0 < i) ->
+       (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
   (* Else *)
-  Have: 10 <= i_1.
+  Have: 10 <= i.
   (* Loop assigns 'CHECK' *)
-  Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
-      (forall i_3 : Z. ((i_3 != 0) -> ((i_3 != 2) -> ((i_3 != 4) ->
-       ((0 <= i_3) -> ((i_3 <= 9) -> ((a[i_3]=true) <-> (v[i_3]=true)))))))) /\
-      (forall i_3 : Z. ((i_3 != 0) -> ((i_3 != 2) -> ((i_3 != 4) ->
-       ((0 <= i_3) -> ((i_3 <= 9) -> ((s.F1_S_a)[i_3] = v_1[i_3]))))))) /\
-      (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((v[i_3]=true) ->
-       (((i_3 = 0) \/ (i_3 = 2) \/ (i_3 = 4)) -> (a[i_3]=true)))))).
+  Have: ((s.F1_S_i) = 0) /\
+      (forall i_2 : Z. ((i_2 != 0) -> ((i_2 != 2) -> ((i_2 != 4) ->
+       ((0 <= i_2) -> ((i_2 <= 9) -> ((s.F1_S_a)[i_2] = v_1[i_2]))))))).
   (* Else *)
-  Have: 10 <= i_2.
+  Have: 10 <= i_1.
 }
-Prove: (a[i]=true).
+Prove: ((Init_s_0.Init_F1_S_i)=true) /\
+    (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+     ((Init_s_0.Init_F1_S_a)[i_2]=true)))).
 
 ------------------------------------------------------------
 
@@ -255,29 +250,24 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 38):
-Let a = Init_s_0.Init_F1_S_a.
 Assume {
-  Have: 0 <= i.
-  Have: i <= 9.
-  Type: is_sint32(i_1) /\ is_sint32(i_2).
+  Type: is_sint32(i) /\ is_sint32(i_1).
   (* Invariant *)
-  Have: (0 <= i_1) /\ (i_1 <= 10) /\
-      (((0 < i_1) ->
-       (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
+  Have: (0 <= i) /\ (i <= 10) /\
+      (((0 < i) ->
+       (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
   (* Else *)
-  Have: 10 <= i_1.
+  Have: 10 <= i.
   (* Loop assigns 'CHECK' *)
-  Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
-      (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
-       (((i_3 <= 0) \/ (5 <= i_3)) -> ((a[i_3]=true) <-> (v[i_3]=true)))))) /\
-      (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
-       (((i_3 <= 0) \/ (5 <= i_3)) -> ((s.F1_S_a)[i_3] = v_1[i_3]))))) /\
-      (forall i_3 : Z. ((0 < i_3) -> ((0 <= i_3) -> ((i_3 <= 4) ->
-       ((i_3 <= 9) -> ((v[i_3]=true) -> (a[i_3]=true))))))).
+  Have: ((s.F1_S_i) = 0) /\
+      (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+       (((i_2 <= 0) \/ (5 <= i_2)) -> ((s.F1_S_a)[i_2] = v_1[i_2]))))).
   (* Else *)
-  Have: 10 <= i_2.
+  Have: 10 <= i_1.
 }
-Prove: (a[i]=true).
+Prove: ((Init_s_0.Init_F1_S_i)=true) /\
+    (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+     ((Init_s_0.Init_F1_S_a)[i_2]=true)))).
 
 ------------------------------------------------------------
 

src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle

@@ -7,7 +7,7 @@
 [wp] [Qed] Goal typed_initialize_loop_invariant_CHECK_established : Valid
 [wp] [Alt-Ergo] Goal typed_initialize_check_CHECK : Valid
 [wp] [Qed] Goal typed_initialize_loop_assigns : Valid
-[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Unsuccess
 [wp] [Qed] Goal typed_range_loop_assigns_part1 : Valid
 [wp] [Qed] Goal typed_range_loop_assigns_part2 : Valid
 [wp] [Alt-Ergo] Goal typed_field_check_CHECK : Valid
@@ -17,7 +17,7 @@
 [wp] [Alt-Ergo] Goal typed_index_check_CHECK : Valid
 [wp] [Qed] Goal typed_index_loop_assigns_part1 : Valid
 [wp] [Qed] Goal typed_index_loop_assigns_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Unsuccess
 [wp] [Qed] Goal typed_descr_loop_assigns_part1 : Valid
 [wp] [Alt-Ergo] Goal typed_descr_loop_assigns_part2 : Valid
 [wp] [Qed] Goal typed_descr_loop_assigns_part3 : Valid
@@ -25,16 +25,16 @@
 [wp] [Qed] Goal typed_descr_loop_assigns_part5 : Valid
 [wp] [Alt-Ergo] Goal typed_comp_check_CHECK : Valid
 [wp] [Qed] Goal typed_comp_loop_assigns : Valid
-[wp] Proved goals:   22 / 22
+[wp] Proved goals:   20 / 22
   Qed:            13 
-  Alt-Ergo:        9
+  Alt-Ergo:        7  (unsuccess: 2)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   initialize                2        2        4       100%
-  range                     2        1        3       100%
+  range                     2        -        3      66.7%
   field                     1        1        2       100%
   array                     1        1        2       100%
   index                     2        1        3       100%
-  descr                     4        2        6       100%
+  descr                     4        1        6      83.3%
   comp                      1        1        2       100%
 ------------------------------------------------------------