[WP] Review of the sequent decomposition

src/plugins/wp/Conditions.ml

@@ -447,7 +447,10 @@ let rec exist_intro p =
       let _,t = e_open ~pool ~exists:true
           ~forall:false ~lambda:false (e_prop p) in
       exist_intro (F.p_bool t)
-  | _ ->
+  | _ -> (* Note: Qed implement De Morgan rules
+            such that [p] cannot match the
+            decomposable representations:
+            Not Or, Not Imply, Not Forall *)
       if Wp_parameters.Prenex.get ()
       then prenex_intro p
       else p
@@ -463,7 +466,11 @@ let rec exist_intros = function
           let _,t = F.QED.e_open ~pool ~exists:true
               ~forall:false ~lambda:false (e_prop p) in
           exist_intros ((F.p_bool t)::hs)
-      | _ -> p::(exist_intros hs)
+      | _ -> (* Note: Qed implement De Morgan rules
+                such that [p] cannot match the
+                decomposable representations:
+                Not Or, Not Imply, Not Forall *)
+          p::(exist_intros hs)
     end
 
 (* -------------------------------------------------------------------------- *)
@@ -488,8 +495,17 @@ let rec forall_intro p =
           (hp @ hs), (p::ps)) ([],[]) qs
       in (* ORs qs  <==> ORs (hps ==> ps)
                     <==> ((ANDs hps) ==> ORs ps) *)
-      hps, (p_disj ps)
-  | _ -> [] , p
+      let hps,ps = List.fold_left (fun (hs,ps) q ->
+          match F.repr (F.e_prop q) with
+          | Neq _ -> ((F.p_not q)::hs), ps
+          | _ -> hs, (q::ps)) (hps,[]) ps
+      in (* ORs qs <==> ((ANDs hps) ==> ORs ps)) *)
+      hps, (F.p_disj ps)
+  | _ -> (* Note: Qed implement De Morgan rules
+            such that [p] cannot match the
+            decomposable representations:
+            Not And, Not Exists *)
+      [] , p
 
 (* -------------------------------------------------------------------------- *)
 (* --- Constructors                                                       --- *)

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

@@ -39,6 +39,7 @@ Prove: table_of_base(G_z_33) = table_of_base(G_x_31).
 ------------------------------------------------------------
 
 Goal Check 'KO' (file base_offset.i, line 30):
-Prove: table_of_base(G_y_32) != table_of_base(G_x_31).
+Assume { (* Goal *) When: table_of_base(G_y_32) = table_of_base(G_x_31). }
+Prove: false.
 
 ------------------------------------------------------------

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

@@ -153,12 +153,7 @@ Prove: (a = 0) /\ (b = 0).
 ------------------------------------------------------------
 
 Goal Post-condition for 'true' (file bitwise.i, line 78) in 'bor_bool':
-Assume {
-  Type: is_bool(a) /\ is_bool(b).
-  (* Pre-condition for 'true' *)
-  Have: (a = 1) \/ (b = 1).
-}
-Prove: (a != 0) \/ (b != 0).
+Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------

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

@@ -27,7 +27,7 @@
 [wp] [Qed] Goal typed_lshift_shift2_ensures_lsl3 : Valid
 [wp] [Qed] Goal typed_rshift_ensures : Valid
 [wp] [Qed] Goal typed_rshift_shift1_ensures_lsr1 : Valid
-[wp] [Alt-Ergo] Goal typed_bor_bool_true_ensures : Valid
+[wp] [Qed] Goal typed_bor_bool_true_ensures : Valid
 [wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Valid
 [wp] [Qed] Goal typed_band_bool_true_ensures : Valid
 [wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Valid
@@ -42,8 +42,8 @@
 [wp] [Qed] Goal typed_lemma_check_7 : Valid
 [wp] [Qed] Goal typed_cast_uchar_ensures : Valid
 [wp] Proved goals:   38 / 38
-  Qed:            34 
-  Alt-Ergo:        4
+  Qed:            35 
+  Alt-Ergo:        3
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   band                      8        -        8       100%
@@ -52,7 +52,7 @@
   bnot                      1        -        1       100%
   lshift                    4        -        4       100%
   rshift                    2        -        2       100%
-  bor_bool                  -        2        2       100%
+  bor_bool                  1        1        2       100%
   band_bool                 1        1        2       100%
   bxor_bool                 1        1        2       100%
   lemma                     7        -        7       100%

src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle

@@ -174,7 +174,7 @@ Prove: (i + L_f(i)) != b.
 ------------------------------------------------------------
 
 Goal Post-condition 'ko4' in 'forall':
-Prove: (L_f(i) != i_1) \/ P_P(i_1).
+Prove: P_P(L_f(i)).
 
 ------------------------------------------------------------