diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index bfb81802ef8ea8ae06508e9c51c5504ccc8ee483..f2b7746849a3a64caa2dc813c843b392d3a6c0cb 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1754,6 +1754,8 @@ src/plugins/wp/TacInstance.ml: CEA_WP
src/plugins/wp/TacInstance.mli: CEA_WP
src/plugins/wp/TacLemma.ml: CEA_WP
src/plugins/wp/TacLemma.mli: CEA_WP
+src/plugins/wp/TacModMask.ml: CEA_WP
+src/plugins/wp/TacModMask.mli: CEA_WP
src/plugins/wp/TacNormalForm.ml: CEA_WP
src/plugins/wp/TacNormalForm.mli: CEA_WP
src/plugins/wp/TacOverflow.ml: CEA_WP
diff --git a/src/plugins/gui/widget.ml b/src/plugins/gui/widget.ml
index 011a7587d25c304c39598f5352829a4aced8aecd..fdec28d50e0c2323b2aa40f37cf185b1d44a9aab 100644
--- a/src/plugins/gui/widget.ml
+++ b/src/plugins/gui/widget.ml
@@ -211,6 +211,7 @@ class checkbox ~label ?tooltip () =
inherit [bool] selector false as s
inherit! gobj_action button as b
method! set_enabled e = s#set_enabled e ; b#set_enabled e
+ method set_label l = button#set_label l
method! set a = s#set a ; button#set_active a
initializer
begin
diff --git a/src/plugins/gui/widget.mli b/src/plugins/gui/widget.mli
index e208ca117ead4812fb75cb93cfdd545a03f2d52c..1a93c68e7af2934c4311e8ad16908ad5d6829386 100644
--- a/src/plugins/gui/widget.mli
+++ b/src/plugins/gui/widget.mli
@@ -130,6 +130,7 @@ class checkbox : label:string -> ?tooltip:string -> unit ->
object
inherit action
inherit [bool] selector
+ method set_label : string -> unit
end
class switch : ?tooltip:string -> unit ->
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index dbf2df8ce7a15614a2235f8fd11fea846bf7d5be..16c04fc09ca8b761c684cc157dcf6a14bea1870b 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -126,6 +126,16 @@ let match_integer t =
| Logic.Kint c -> c
| _ -> raise Not_found
+let match_to_cint t =
+ match F.repr t with
+ | Logic.Fun( conv , [a] ) -> (to_cint conv), a
+ | _ -> raise Not_found
+
+let match_mod t =
+ match F.repr t with
+ | Logic.Mod (e1, e2) -> e1, e2
+ | _ -> raise Not_found
+
(* integration with qed should be improved! *)
let rec is_positive_or_null e = match F.repr e with
| Logic.Fun( f , [e] ) when Fun.equal f f_lnot -> is_negative e
@@ -137,6 +147,7 @@ let rec is_positive_or_null e = match F.repr e with
| _ -> (* try some improvement first then ask to qed *)
let improved_is_positive_or_null e = match F.repr e with
| Logic.Add es -> List.for_all is_positive_or_null es
+ | Logic.Mod(e1,_) -> is_positive_or_null e1
| _ -> false
in if improved_is_positive_or_null e then true
else match F.is_true (F.e_leq e_zero e) with
@@ -168,7 +179,7 @@ let match_positive_or_null e =
if not (is_positive_or_null e) then raise Not_found;
e
-let match_power2, _match_power2_minus1 =
+let match_power2, match_power2_minus1 =
let highest_bit_number =
let hsb p = if p land 2 = 0 then 0 else 1
in let hsb p = let n = p lsr 2 in if n = 0 then hsb p else 2 + hsb n
@@ -198,7 +209,7 @@ let match_power2, _match_power2_minus1 =
in let match_power2_minus1 e = match F.repr e with
| Logic.Kint z when is_power2 (Integer.succ z) ->
e_zint (highest_bit_number (Integer.succ z))
- | _ -> raise Not_found
+ | _ -> match_power2 (e_add e_one e)
in match_power2, match_power2_minus1
let match_fun op t =
@@ -251,6 +262,7 @@ let match_positive_or_null_integer_arg2 =
let match_integer_extraction = match_list_head match_integer
let match_power2_extraction = match_list_extraction match_power2
+let match_power2_minus1_extraction = match_list_extraction match_power2_minus1
let match_binop_one_extraction binop = match_list_extraction (match_binop_one_arg1 binop)
@@ -601,26 +613,65 @@ let smp_lnot = function
(* --- Comparision with L-AND / L-OR / L-NOT --- *)
(* -------------------------------------------------------------------------- *)
-let smp_leq_with_land a b =
- let es = match_fun f_land a in
- let a1,_ = match_list_head match_positive_or_null_integer es in
- if F.decide (F.e_leq (e_zint a1) b)
+let smp_leq_improved f a b =
+ ignore (match_fun f b) ; (* It must be an improved of [is_positive_or_null f(args)] *)
+ (* a <= 0 && 0 <= f(args) *)
+ if F.decide (F.e_leq a F.e_zero) && is_positive_or_null b
then e_true
else raise Not_found
+let smp_leq_with_land a b =
+ try
+ let es = match_fun f_land a in
+ let a1,_ = match_list_head match_positive_or_null_integer es in
+ if F.decide (F.e_leq (e_zint a1) b)
+ then e_true
+ else raise Not_found
+ with Not_found ->
+ (* a <= 0 && 0 <= (x&y) ==> a <= (x & y) *)
+ smp_leq_improved f_land a b
+
let smp_eq_with_land a b =
let es = match_fun f_land a in
try
- let b1 = match_integer b in
- try (* (b1&~a2)!=0 ==> (b1==(a2&e) <=> false) *)
- let a2,_ = match_integer_extraction es in
- if Integer.is_zero (Integer.logand b1 (Integer.lognot a2))
- then raise Not_found ;
- e_false
- with Not_found when b == e_minus_one ->
- (* -1==(a1&a2) <=> (-1==a1 && -1==a2) *)
- F.e_and (List.map (e_eq b) es)
- with Not_found -> introduction_bit_test_positive es b
+ try
+ let b1 = match_integer b in
+ try (* (b1&~a2)!=0 ==> (b1==(a2&e) <=> false) *)
+ let a2,_ = match_integer_extraction es in
+ if Integer.is_zero (Integer.logand b1 (Integer.lognot a2))
+ then raise Not_found ;
+ e_false
+ with Not_found when b == e_minus_one ->
+ (* -1==(a1&a2) <=> (-1==a1 && -1==a2) *)
+ F.e_and (List.map (e_eq b) es)
+ with Not_found -> introduction_bit_test_positive es b
+ with Not_found ->
+ try
+ (* k>=0 & b1>=0 ==> (b1 & ((1 << k) -1) == b1 % (1 << k) <==> true) *)
+ let b1,b2 = match_mod b in
+ let k = match_power2 b2 in
+ (* note: a positive or null k is required by match_power2, match_power2_minus1 *)
+ let k',_,es = match_power2_minus1_extraction es in
+ if not ((is_positive_or_null b1) &&
+ (F.decide (F.e_eq k k')) &&
+ (F.decide (F.e_eq b1 (F.e_fun f_land es))))
+ then raise Not_found ;
+ F.e_true
+ with Not_found ->
+ (* k in {8,16,32,64} ==> (b1 & ((1 << k) -1) == to_cint_unsigned_bits(k, b1) <==> true *)
+ let iota,b1 = match_to_cint b in
+ if Ctypes.signed iota then raise Not_found ;
+ let n = Ctypes.i_bits iota in
+ if n = 1 then
+ (* rejects [to_bool()] that is not a modulo *)
+ raise Not_found ;
+ let k',_,es = match_power2_minus1_extraction es in
+ let k' = match_integer k' in
+ let k = Integer.of_int n in
+ if not ((Integer.equal k k') &&
+ (F.decide (F.e_eq b1 (F.e_fun f_land es))))
+ then raise Not_found ;
+ F.e_true
let smp_eq_with_lor a b =
let b1 = match_integer b in
@@ -737,7 +788,11 @@ let smp_eq_with_lsl a b =
try smp_eq_with_lsl_cst a b
with Not_found -> smp_cmp_with_lsl e_eq a b
-let smp_leq_with_lsl a0 b0 = smp_cmp_with_lsl e_leq a0 b0
+let smp_leq_with_lsl a b =
+ try smp_cmp_with_lsl e_leq a b
+ with Not_found ->
+ (* a <= 0 && 0 <= (x << y) ==> a <= (x << y) *)
+ smp_leq_improved f_lsl a b
let smp_eq_with_lsr a0 b0 =
try
@@ -780,6 +835,7 @@ let smp_leq_with_lsr x y =
let k = two_power_k p in
e_leq x (e_div a (e_zint k))
with Not_found ->
+ try
let a,p = match_fun f_lsr x |> match_positive_or_null_integer_arg2 in
(* (a >> p) <= y with p >= 0 *)
if y == e_zero then
@@ -789,6 +845,10 @@ let smp_leq_with_lsr x y =
(* p >= 0 ==> ( (a >> p) <= y <==> a/(2**p) <= y ) *)
let k = two_power_k p in
e_leq (e_div a (e_zint k)) y
+ with Not_found ->
+ (* x <= y && 0 <= (a&b) ==> x <= (a >> b) *)
+ smp_leq_improved f_lsr x y
+
(* Rewritting at export *)
let bitk_export k e = F.e_fun ~result:Logic.Bool f_bit_export [e;k]
@@ -818,10 +878,10 @@ let () =
no creation of [e_fun f_bit_stdlib args] *)
let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in
let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in
- let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot smp_lnot in
- let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
+ let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot smp_lnot ~leq:(smp_leq_improved f_lnot) in
+ let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor ~leq:(smp_leq_improved f_lxor)
(smp2 f_lxor Integer.logxor) in
- let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor
+ let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor ~leq:(smp_leq_improved f_lor)
(smp2 f_lor Integer.logor) in
let bi_land = mk_builtin "f_land" f_land ~eq:smp_eq_with_land ~leq:smp_leq_with_land
smp_land in
diff --git a/src/plugins/wp/Cint.mli b/src/plugins/wp/Cint.mli
index b4868c855f417c28f2984ccc3c879795ef2540d1..e889cc7d28636556e4bd95d472db3dbdd01da4f6 100644
--- a/src/plugins/wp/Cint.mli
+++ b/src/plugins/wp/Cint.mli
@@ -77,6 +77,11 @@ val f_bits : lfun list (** All bit-test functions *)
val bit_test : term -> int -> term
+(** Matchers *)
+
+val match_power2 : term -> term
+val match_power2_minus1 : term -> term
+
(** Simplifiers *)
val is_cint_simplifier: simplifier
diff --git a/src/plugins/wp/GuiTactic.ml b/src/plugins/wp/GuiTactic.ml
index cd14d8126cfd5ca69012706ae4ba04ef3ff8c631..8484deedffa91668367340b37887826381e581a7 100644
--- a/src/plugins/wp/GuiTactic.ml
+++ b/src/plugins/wp/GuiTactic.ml
@@ -89,7 +89,7 @@ class checkbox
begin
Wutil.on enabled button#set_visible ;
Wutil.on tooltip button#set_tooltip ;
- ignore title ;
+ Wutil.on title button#set_label ;
ignore filter ;
ignore vmin ;
ignore vmax ;
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 72ad09daf3b043ff114ba3ab2f89fdfc1681c145..d9c8c5f2903af5bc661e3015e2dcbba5f025a0bd 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -90,7 +90,7 @@ PLUGIN_CMO:= \
TacArray TacCompound TacUnfold \
TacHavoc TacInstance TacLemma \
TacFilter TacCut WpTac TacNormalForm \
- TacRewrite TacBitwised TacBitrange TacBittest TacShift \
+ TacRewrite TacBitwised TacBitrange TacBittest TacModMask TacShift \
TacSequence \
TacCongruence TacOverflow Auto \
ProofSession ProofScript ProofEngine \
diff --git a/src/plugins/wp/TacModMask.ml b/src/plugins/wp/TacModMask.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ac36c191eb812f8cee19bef219f23bfd4eaaa55c
--- /dev/null
+++ b/src/plugins/wp/TacModMask.ml
@@ -0,0 +1,123 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Tactical
+
+let title_no_revert = "Revert (current: a & m -> a % m+1)"
+let title_revert = "Revert (current: m & a -> a % m+1)"
+
+let v_revert,p_revert =
+ Tactical.checkbox ~id:"Wp.modmask.revert"
+ ~title:title_no_revert
+ ~descr:"Changes operands for modulo"
+ ~default:false ()
+
+class modmask =
+ object(self)
+ inherit Tactical.make
+ ~id:"Wp.modmask"
+ ~title:"Mod-Mask"
+ ~descr:"Converts modulo from/to bitmask"
+ ~params:[p_revert]
+
+ method select feedback selection =
+ let open Lang.N in
+ let open Lang.F in
+ let open Qed.Logic in
+
+ let e = Tactical.selected selection in
+ let at = Tactical.at selection in
+
+ let on_cond = Tactical.condition in
+ let replace_with d v = Tactical.rewrite ?at [ d, Lang.F.p_true, e, v ] in
+
+ let update_title ~hard =
+ feedback#set_title "Mod-Mask%s" (if hard then " (hard)" else "")
+ in
+ let update_field ~enabled =
+ let revert = self#get_field v_revert in
+ let title = if revert then title_revert else title_no_revert in
+ feedback#update_field ~enabled v_revert ;
+ feedback#update_field ~title v_revert
+ in
+ let update_display ~hard ~active_field =
+ update_title ~hard ;
+ update_field ~enabled:active_field
+ in
+ match Lang.F.repr e with
+ | Mod(a, m) ->
+ begin
+ try
+ let m = Cint.l_lsl e_one @@ Cint.match_power2 m in
+ let n = Cint.l_and a (m - e_one) in
+ let cond = a >= e_zero in
+
+ update_display ~hard:false ~active_field:false ;
+ Applicable (on_cond "Mask Guard" cond @@ replace_with "Mask" n)
+
+ with Not_found ->
+ let power_of_2 =
+ let v = Lang.freshvar ~basename:"n" Lang.t_int in
+ let tv = e_var v in
+ p_exists [v] (e_zero <= tv && m = Cint.l_lsl e_one tv)
+ in
+ let cond = (a >= e_zero && e_zero < m && power_of_2) in
+ let n = Cint.l_and a (m - e_one) in
+
+ update_display ~hard:true ~active_field:false ;
+ Applicable (on_cond "Mask Guard" cond @@ replace_with "Mask" n)
+ end
+
+ | Fun( f , [ a ; b ] ) when Lang.Fun.equal f Cint.f_land ->
+ begin
+ try
+ let a, m =
+ try b, Cint.match_power2_minus1 a
+ with Not_found -> a, Cint.match_power2_minus1 b
+ in
+
+ let cond = a >= e_zero in
+ let n = a mod (Cint.l_lsl e_one m) in
+
+ update_display ~hard:false ~active_field:false ;
+ Applicable (on_cond "Mod Guard" cond @@ replace_with "Mod" n)
+
+ with Not_found ->
+ let a, m = if self#get_field v_revert then b, a else a, b in
+ let plus_1_power_of_2 =
+ let v = Lang.freshvar ~basename:"n" Lang.t_int in
+ let tv = e_var v in
+ p_exists [v] (e_zero <= tv && m + e_one = Cint.l_lsl e_one tv)
+ in
+ let cond = (a >= e_zero && e_zero <= m && plus_1_power_of_2) in
+ let n = a mod (m + e_one) in
+
+ update_display ~hard:true ~active_field:true ;
+ Applicable (on_cond "Mod Guard" cond @@ replace_with "Mod" n)
+ end
+
+ | _ ->
+ update_display ~hard:false ~active_field:false ;
+ Not_applicable
+ end
+
+let modmask = Tactical.export (new modmask)
diff --git a/src/plugins/wp/TacModMask.mli b/src/plugins/wp/TacModMask.mli
new file mode 100644
index 0000000000000000000000000000000000000000..fb0f0f4daf14c2bea477c92e0e0dad1ffa8895ec
--- /dev/null
+++ b/src/plugins/wp/TacModMask.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+val modmask : Tactical.tactical
diff --git a/src/plugins/wp/tests/wp_acsl/bitwise.i b/src/plugins/wp/tests/wp_acsl/bitwise.i
index a77559d8fc218a0afcc8f465b092337fc99a6594..b2e5594f27096dbe8e31f400e04a8cc75ee1abce 100644
--- a/src/plugins/wp/tests/wp_acsl/bitwise.i
+++ b/src/plugins/wp/tests/wp_acsl/bitwise.i
@@ -101,7 +101,7 @@ _Bool band_bool(_Bool a, _Bool b) { return (_Bool)(((int)a & (int)b) != 0); }
*/
_Bool bxor_bool(_Bool a, _Bool b) { return (_Bool)(((int)a ^ (int)b) != 0); }
-void lemma(unsigned a, unsigned b) {
+void lemma(unsigned a, unsigned b, unsigned k) {
//@ check zbit: a1: ~(a + ~a) == 0;
//@ check zbit: a2: ~(a | ~a) == 0;
//@ check zbit: a3: (a & ~a) == 0;
@@ -110,4 +110,23 @@ void lemma(unsigned a, unsigned b) {
//@ check (~a --> a) == a;
//@ check (a --> ~a) == ~a;
//@ check (~a == ~b) ==> (a == b);
+
+ //@ check zbit: a4: ( a & b & 0xFF ) == ( (a & b) % 0x100 );
+ /* note: a5 is not simplified because Qed cannot infer that a&b is positive
+ */
+
+ //@ check ( a & (85 % b) & 0xFF ) == ( (a & (85 % b)) % 0x100 );
+
+ //@ check zbit: a5: ( a & b & 77 & ((1 << k)-1) ) == ( (a & b & 77) % (1 << k) );
+ /* note: a4 is not simplified because Qed cannot infer that k is positive
+ */
+
+ //@ check ( a & b & 77 & ((1 << (k & 55))-1) ) == ( (a & b & 77) % (1 << (k & 55)) );
+
+}
+
+//@ ensures \result == (x & 0xFF) ;
+unsigned char cast_uchar(int x) {
+ unsigned char c = x;
+ return c;
}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
index b9c417ef5fd0e15877f3f89622b9b6966da49a24..232b2653404ec97a49e685a92afecc0955b00594 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
@@ -218,6 +218,14 @@ Assume {
}
Prove: b != a.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function cast_uchar
+------------------------------------------------------------
+
+Goal Post-condition (file bitwise.i, line 128) in 'cast_uchar':
+Prove: true.
+
------------------------------------------------------------
------------------------------------------------------------
Function lemma
@@ -264,6 +272,29 @@ Prove: true.
Goal Check (file bitwise.i, line 112):
Prove: true.
+------------------------------------------------------------
+
+Goal Check 'zbit,a4' (file bitwise.i, line 114):
+Assume { Type: is_uint32(a) /\ is_uint32(b). }
+Prove: (land(a, b) % 256) = land(255, land(a, b)).
+
+------------------------------------------------------------
+
+Goal Check (file bitwise.i, line 118):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'zbit,a5' (file bitwise.i, line 120):
+Let x = lsl(1, k).
+Assume { Type: is_uint32(a) /\ is_uint32(b) /\ is_uint32(k). }
+Prove: (land(77, land(a, b)) % x) = land(77, land(a, land(b, x - 1))).
+
+------------------------------------------------------------
+
+Goal Check (file bitwise.i, line 124):
+Prove: true.
+
------------------------------------------------------------
------------------------------------------------------------
Function lshift
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
index c821ec7b2ef31c0fcd7daf7cbdb2d2f45ba518bd..413c2326caae6ae63dcdeaa67818f7b7376c90ad 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing bitwise.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 35 goals scheduled
+[wp] 38 goals scheduled
[wp] [Qed] Goal typed_band_ensures : Valid
[wp] [Qed] Goal typed_band_ensures_band0 : Valid
[wp] [Qed] Goal typed_band_bit0_ensures_band1 : Valid
@@ -38,8 +38,11 @@
[wp] [Qed] Goal typed_lemma_check_3 : Valid
[wp] [Qed] Goal typed_lemma_check_4 : Valid
[wp] [Qed] Goal typed_lemma_check_5 : Valid
-[wp] Proved goals: 35 / 35
- Qed: 31
+[wp] [Qed] Goal typed_lemma_check_6 : Valid
+[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
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
@@ -52,5 +55,6 @@
bor_bool - 2 2 100%
band_bool 1 1 2 100%
bxor_bool 1 1 2 100%
- lemma 5 - 5 100%
+ lemma 7 - 7 100%
+ cast_uchar 1 - 1 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
index 6c74a498337a8547eb0dacd1cf85f2c6177e638a..18231f2787cfacbce7f1fd426b27d0a7d6beaf6e 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
@@ -10,8 +10,7 @@ Goal Preservation of Invariant 'RANGE' (file issue_751.i, line 7):
Let x = land(3840, R).
Let x_1 = x / 256.
Assume {
- Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(1 + j) /\
- is_sint32(lsr(x, 8)).
+ Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(1 + j).
(* Pre-condition *)
Have: (0 < x) /\ (x <= 2303).
(* Invariant 'RANGE' *)
@@ -36,18 +35,17 @@ Prove: true.
Goal Loop assigns (file issue_751.i, line 8) (2/2):
Effect at line 11
Let x = land(3840, R).
-Let x_1 = lsr(x, 8).
-Let x_2 = j - 1.
+Let x_1 = j - 1.
Assume {
- Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(x_2) /\ is_sint32(x_1).
+ Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(x_1).
(* Heap *)
Type: (region(Data_0.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: !invalid(Malloc_0, shift_sint32(Data_0, x_2), 1).
+ When: !invalid(Malloc_0, shift_sint32(Data_0, x_1), 1).
(* Pre-condition *)
Have: (0 < x) /\ (x <= 2303).
(* Invariant 'RANGE' *)
- Have: (0 < j) /\ (j <= (1 + x_1)).
+ Have: (0 < j) /\ (j <= (1 + lsr(x, 8))).
(* Then *)
Have: j <= (x / 256).
}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
index 77438629a177d10c967e936ebf34b1db7e8cbf09..c4a3730943a5705f49d9a0510a3f8b28c275b328 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
@@ -1,32 +1,11 @@
-[ { "header": "Bitwise Eq.", "tactic": "Wp.bitwised",
+[ { "prover": "Alt-Ergo:2.2.0", "verdict": "timeout", "time": 10. },
+ { "prover": "script", "verdict": "valid" },
+ { "header": "Bitwise Eq.", "tactic": "Wp.bitwised",
"params": { "Wp.bitwised.range": 32 },
- "select": { "select": "inside-goal", "occur": 0,
+ "select": { "select": "clause-goal",
"target": "(land 4294967295 x_0)=x_0",
"pattern": "=land$x4294967295$x" },
- "children": { "range": [ { "header": "Split", "tactic": "Wp.split",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "(0<=x_0) /\\ (0<=(land 4294967295 x_0)) /\\ (x_0<=4294967295)",
- "pattern": "&<=<=<=0$x0land$x42949672954294967295" },
- "children": { "Goal 1/3": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid",
- "time": 0.0095,
- "steps": 14 } ],
- "Goal 2/3": [ { "header": "Bit Range",
- "tactic": "Wp.bitrange",
- "params":
- { "positive-land": true,
- "positive-lor": true },
- "select":
- { "select": "clause-goal",
- "target": "0<=(land 4294967295 x_0)",
- "pattern": "<=0land4294967295$x" },
- "children":
- { "bit-range":
- [ { "prover": "qed",
- "verdict": "valid" } ] } } ],
- "Goal 3/3": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid",
- "time": 0.01,
- "steps": 14 } ] } } ],
+ "children": { "range": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0054,
+ "steps": 15 } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/modmask.i b/src/plugins/wp/tests/wp_tip/modmask.i
new file mode 100644
index 0000000000000000000000000000000000000000..1970a5e62026c8ec79c5414ac01097565831704b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/modmask.i
@@ -0,0 +1,18 @@
+/* run.config
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+
+/*@
+ check lemma and_modulo_us_255:
+ \forall unsigned short us ; (us & 0xFF) == us % 0x100 ;
+*/
+
+/*@
+ check lemma and_modulo_u:
+ \forall unsigned us, integer shift;
+ 0 <= shift < (sizeof(us) * 8) ==> (us & ((1 << shift) - 1)) == us % (1 << shift);
+*/
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..dd1cd3edf7d9ef503650337d4d5bca8a6a5e038f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
@@ -0,0 +1,79 @@
+# frama-c -wp [...]
+[kernel] Parsing modmask.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 2 goals scheduled
+[wp:script:allgoals]
+ Lemma and_modulo_u:
+ Prove: let x_0 = (lsl 1 shift_0) in
+ (0<=shift_0) -> (shift_0<=31) -> (is_uint32 us_0)
+ -> ((us_0 mod x_0)=(land us_0 (x_0-1)))
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ Lemma and_modulo_us_255:
+ Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-0 (generated):
+ Let x = lsl(1, shift_0).
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: (0 <= us_0) /\ (0 < x) /\ (exists i : Z. (lsl(1, i) = x) /\ (0 <= i)).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-1 (generated):
+ Prove: true.
+ Prover Qed returns Valid
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_us_255 subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-0 (generated):
+ Assume { Have: is_uint16(us_0). }
+ Prove: 0 <= us_0.
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_us_255 subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-1 (generated):
+ Prove: true.
+ Prover Qed returns Valid
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-2 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: 0 <= us_0.
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-3 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: 0 < lsl(1, shift_0).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-4 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_u : Valid
+[wp] Proved goals: 2 / 2
+ Qed: 0
+ Script: 2
+[wp] Updated session with 2 new valid scripts.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
new file mode 100644
index 0000000000000000000000000000000000000000..e40e8863e3cf66cd9c1c3c6e4d1f0fa5d083d726
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
@@ -0,0 +1,162 @@
+[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
+ "params": { "Wp.modmask.revert": false },
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "us_0 mod (lsl 1 shift_0)",
+ "pattern": "%$uslsl1$shift" },
+ "children": { "Mask Guard": [ { "header": "Split", "tactic": "Wp.split",
+ "params": {},
+ "select": { "select": "clause-goal",
+ "target": "let x_0 = (lsl 1 shift_0) in\n(0<=us_0) /\\ (0<x_0) /\\ (exists i_0:int.\n ((lsl 1 i_0)=x_0) /\\ (0<=i_0))",
+ "pattern": "&<=<\\E0$us0lsl1$shiftlsl011$shift" },
+ "children": { "Goal 1/3": [ { "header": "Definition",
+ "tactic": "Wp.unfold",
+ "params": {},
+ "select":
+ { "select": "clause-step",
+ "at": 2,
+ "kind": "have",
+ "target": "(is_uint32 us_0)",
+ "pattern": "is_uint32$us" },
+ "children":
+ { "Unfold 'is_uint32'":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 2/3": [ { "header": "Range",
+ "tactic": "Wp.range",
+ "params":
+ { "inf": 0,
+ "sup": 31 },
+ "select":
+ { "select": "inside-goal",
+ "occur": 0,
+ "target": "shift_0",
+ "pattern": "$shift" },
+ "children":
+ { "Lower 0":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 0":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 1":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 2":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 3":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 4":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 5":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 6":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 7":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 8":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 9":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 10":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 11":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 12":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 13":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 14":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 15":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 16":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 17":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 18":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 19":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 20":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 21":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 22":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 23":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 24":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 25":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 26":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 27":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 28":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 29":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 30":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 31":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Upper 31":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 3/3": [ { "header": "Instance",
+ "tactic": "Wp.instance",
+ "params":
+ { "P1":
+ { "select": "inside-goal",
+ "occur": 0,
+ "target": "shift_0",
+ "pattern": "$shift" },
+ "P2": null,
+ "P3": null,
+ "P4": null,
+ "P5": null,
+ "P6": null,
+ "P7": null,
+ "P8": null,
+ "P9": null,
+ "P10": null },
+ "select":
+ { "select": "clause-goal",
+ "target": "exists i_0:int. ((lsl 1 i_0)=(lsl 1 shift_0)) /\\ (0<=i_0)",
+ "pattern": "\\Elsl011$shift" },
+ "children":
+ { "Witness":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ],
+ "Mask": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
new file mode 100644
index 0000000000000000000000000000000000000000..0232433c576b0cb20e7c6108b28bec094abaa799
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
@@ -0,0 +1,14 @@
+[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
+ "params": { "Wp.modmask.revert": false },
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "us_0 mod 256", "pattern": "%$us256" },
+ "children": { "Mask Guard": [ { "header": "Definition",
+ "tactic": "Wp.unfold", "params": {},
+ "select": { "select": "clause-step",
+ "at": 0, "kind": "have",
+ "target": "(is_uint16 us_0)",
+ "pattern": "is_uint16$us" },
+ "children": { "Unfold 'is_uint16'":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Mask": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..dd1cd3edf7d9ef503650337d4d5bca8a6a5e038f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
@@ -0,0 +1,79 @@
+# frama-c -wp [...]
+[kernel] Parsing modmask.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 2 goals scheduled
+[wp:script:allgoals]
+ Lemma and_modulo_u:
+ Prove: let x_0 = (lsl 1 shift_0) in
+ (0<=shift_0) -> (shift_0<=31) -> (is_uint32 us_0)
+ -> ((us_0 mod x_0)=(land us_0 (x_0-1)))
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ Lemma and_modulo_us_255:
+ Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-0 (generated):
+ Let x = lsl(1, shift_0).
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: (0 <= us_0) /\ (0 < x) /\ (exists i : Z. (lsl(1, i) = x) /\ (0 <= i)).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-1 (generated):
+ Prove: true.
+ Prover Qed returns Valid
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_us_255 subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-0 (generated):
+ Assume { Have: is_uint16(us_0). }
+ Prove: 0 <= us_0.
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_us_255 subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-1 (generated):
+ Prove: true.
+ Prover Qed returns Valid
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-2 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: 0 <= us_0.
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-3 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: 0 < lsl(1, shift_0).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-4 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_u : Valid
+[wp] Proved goals: 2 / 2
+ Qed: 0
+ Script: 2
+[wp] Updated session with 2 new valid scripts.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
new file mode 100644
index 0000000000000000000000000000000000000000..7d2e4b041e8f70d94528bc04cf06fc7d49bbbb6e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
@@ -0,0 +1,162 @@
+[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
+ "params": { "Wp.modmask.revert": false },
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "(land us_0 ((lsl 1 shift_0)-1))",
+ "pattern": "land$us+-1lsl1$shift" },
+ "children": { "Mod Guard": [ { "header": "Split", "tactic": "Wp.split",
+ "params": {},
+ "select": { "select": "clause-goal",
+ "target": "let x_0 = (lsl 1 shift_0) in\n(0<=us_0) /\\ (0<x_0) /\\ (exists i_0:int.\n ((lsl 1 i_0)=x_0) /\\ (0<=i_0))",
+ "pattern": "&<=<\\E0$us0lsl1$shiftlsl011$shift" },
+ "children": { "Goal 1/3": [ { "header": "Definition",
+ "tactic": "Wp.unfold",
+ "params": {},
+ "select":
+ { "select": "clause-step",
+ "at": 2,
+ "kind": "have",
+ "target": "(is_uint32 us_0)",
+ "pattern": "is_uint32$us" },
+ "children":
+ { "Unfold 'is_uint32'":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 2/3": [ { "header": "Range",
+ "tactic": "Wp.range",
+ "params":
+ { "inf": 0,
+ "sup": 31 },
+ "select":
+ { "select": "inside-goal",
+ "occur": 0,
+ "target": "shift_0",
+ "pattern": "$shift" },
+ "children":
+ { "Lower 0":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 0":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 1":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 2":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 3":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 4":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 5":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 6":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 7":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 8":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 9":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 10":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 11":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 12":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 13":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 14":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 15":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 16":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 17":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 18":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 19":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 20":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 21":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 22":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 23":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 24":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 25":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 26":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 27":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 28":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 29":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 30":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 31":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Upper 31":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 3/3": [ { "header": "Instance",
+ "tactic": "Wp.instance",
+ "params":
+ { "P1":
+ { "select": "inside-goal",
+ "occur": 0,
+ "target": "shift_0",
+ "pattern": "$shift" },
+ "P2": null,
+ "P3": null,
+ "P4": null,
+ "P5": null,
+ "P6": null,
+ "P7": null,
+ "P8": null,
+ "P9": null,
+ "P10": null },
+ "select":
+ { "select": "clause-goal",
+ "target": "exists i_0:int. ((lsl 1 i_0)=(lsl 1 shift_0)) /\\ (0<=i_0)",
+ "pattern": "\\Elsl011$shift" },
+ "children":
+ { "Witness":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ],
+ "Mod": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
new file mode 100644
index 0000000000000000000000000000000000000000..a56490bac7af0b6011890ef00ef38f25fa4cd251
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
@@ -0,0 +1,14 @@
+[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
+ "params": { "Wp.modmask.revert": false },
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "(land 255 us_0)", "pattern": "land255$us" },
+ "children": { "Mod Guard": [ { "header": "Definition",
+ "tactic": "Wp.unfold", "params": {},
+ "select": { "select": "clause-step",
+ "at": 0, "kind": "have",
+ "target": "(is_uint16 us_0)",
+ "pattern": "is_uint16$us" },
+ "children": { "Unfold 'is_uint16'":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Mod": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
index 558b45d9fdf74924a1face948576f5abfc6fa618..7454740a0f188b3058081228b4a2837ba6beeb9f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
@@ -147,8 +147,7 @@ Prove: true.
------------------------------------------------------------
Goal Assertion 'ok' (file unit_bitwise.c, line 117):
-Let x = land(1, a). Assume { Type: is_uint8(a) /\ is_uint8(x). }
-Prove: 0 <= x.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -161,8 +160,7 @@ Prove: true.
------------------------------------------------------------
Goal Assertion 'ok' (file unit_bitwise.c, line 52):
-Let x = land(1, a). Assume { Type: is_uint32(a) /\ is_uint32(x). }
-Prove: 0 <= x.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -175,8 +173,7 @@ Prove: true.
------------------------------------------------------------
Goal Assertion 'ok' (file unit_bitwise.c, line 170):
-Let x = land(1, a). Assume { Type: is_uint64(a) /\ is_uint64(x). }
-Prove: 0 <= x.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -189,8 +186,7 @@ Prove: true.
------------------------------------------------------------
Goal Assertion 'ok' (file unit_bitwise.c, line 165):
-Let x = land(1, a). Assume { Type: is_uint16(a) /\ is_uint16(x). }
-Prove: 0 <= x.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle
index 5c838689f12914c9e16edb03cb53b10e8ec0312c..8c72c29788e6c5de7430921640c4ca0c5b4297fd 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle
@@ -29,7 +29,7 @@
[wp] [Qed] Goal typed_lshift_int_ensures_ok : Valid
[wp] [Qed] Goal typed_rshift_int_ensures_ok : Valid
[wp] [Qed] Goal typed_band1_uint_assert_ok : Valid
-[wp] [Alt-Ergo] Goal typed_band1_uint_assert_ok_2 : Valid
+[wp] [Qed] Goal typed_band1_uint_assert_ok_2 : Valid
[wp] [Qed] Goal typed_band_uint_ensures_ok : Valid
[wp] [Qed] Goal typed_bor_uint_ensures_ok : Valid
[wp] [Qed] Goal typed_bxor_uint_ensures_ok : Valid
@@ -44,7 +44,7 @@
[wp] [Qed] Goal typed_lshift_char_ensures_ok : Valid
[wp] [Qed] Goal typed_rshift_char_ensures_ok : Valid
[wp] [Qed] Goal typed_band1_uchar_assert_ok : Valid
-[wp] [Alt-Ergo] Goal typed_band1_uchar_assert_ok_2 : Valid
+[wp] [Qed] Goal typed_band1_uchar_assert_ok_2 : Valid
[wp] [Alt-Ergo] Goal typed_band_uchar_ensures_ok : Valid
[wp] [Qed] Goal typed_bor_uchar_ensures_ok : Valid
[wp] [Qed] Goal typed_bxor_uchar_ensures_ok : Valid
@@ -53,9 +53,9 @@
[wp] [Qed] Goal typed_lshift_uchar_ensures_ok : Valid
[wp] [Alt-Ergo] Goal typed_rshift_uchar_ensures_ok : Valid
[wp] [Qed] Goal typed_band1_ushort_assert_ok : Valid
-[wp] [Alt-Ergo] Goal typed_band1_ushort_assert_ok_2 : Valid
+[wp] [Qed] Goal typed_band1_ushort_assert_ok_2 : Valid
[wp] [Qed] Goal typed_band1_ulong_assert_ok : Valid
-[wp] [Alt-Ergo] Goal typed_band1_ulong_assert_ok_2 : Valid
+[wp] [Qed] Goal typed_band1_ulong_assert_ok_2 : Valid
[wp] [Qed] Goal typed_cast_ensures_ok : Valid
[wp] [Qed] Goal typed_cast_assert_ok : Valid
[wp] [Qed] Goal typed_cast_assert_ok_2 : Valid
@@ -65,8 +65,8 @@
[wp] [Qed] Goal typed_cast_assert_ok_6 : Valid
[wp] [Qed] Goal typed_cast_assert_ok_7 : Valid
[wp] Proved goals: 61 / 61
- Qed: 41
- Alt-Ergo: 20
+ Qed: 45
+ Alt-Ergo: 16
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma 10 8 18 100%
@@ -78,7 +78,7 @@
bnot_int 1 - 1 100%
lshift_int 1 - 1 100%
rshift_int 1 - 1 100%
- band1_uint 1 1 2 100%
+ band1_uint 2 - 2 100%
band_uint 1 - 1 100%
bor_uint 1 - 1 100%
bxor_uint 1 1 2 100%
@@ -91,14 +91,14 @@
bnot_char - 1 1 100%
lshift_char 1 - 1 100%
rshift_char 1 - 1 100%
- band1_uchar 1 1 2 100%
+ band1_uchar 2 - 2 100%
band_uchar - 1 1 100%
bor_uchar 1 - 1 100%
bxor_uchar 1 1 2 100%
bnot_uchar 1 - 1 100%
lshift_uchar 1 - 1 100%
rshift_uchar - 1 1 100%
- band1_ushort 1 1 2 100%
- band1_ulong 1 1 2 100%
+ band1_ushort 2 - 2 100%
+ band1_ulong 2 - 2 100%
cast 8 - 8 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
deleted file mode 100644
index aa52fbebd0ceb26b098784cbb877f8bdadb051e6..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_138) /\\ (i_1<=i_139) /\\ (0<=i_0) /\\ (i_138<=i_0) /\\ (i_139<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0088,
- "steps": 24 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0116,
- "steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
deleted file mode 100644
index aa52fbebd0ceb26b098784cbb877f8bdadb051e6..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_138) /\\ (i_1<=i_139) /\\ (0<=i_0) /\\ (i_138<=i_0) /\\ (i_139<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0088,
- "steps": 24 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0116,
- "steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
deleted file mode 100644
index 820cbd3fc5e4f803e38f914bb981e386dfc27b4a..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0124,
- "steps": 43 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0121,
- "steps": 43 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
deleted file mode 100644
index abaf79ffd0a939aaa9f4c60806bc8f8890d897a9..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (i_2<=i_3) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (i_3<=i_2) /\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0074,
- "steps": 31 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0078,
- "steps": 31 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
deleted file mode 100644
index a158cb35d7024c69250c2c6f61b9f41654bcb56a..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_158) /\\ (i_1<=i_159) /\\ (0<=i_0) /\\ (i_158<=i_0) /\\ (i_159<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.011,
- "steps": 16 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0092,
- "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
deleted file mode 100644
index 18643516046a339dee16a82e44473e2dc722f1ac..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0099,
- "steps": 42 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0124,
- "steps": 42 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
deleted file mode 100644
index 522d6695a5bb42790b4084770155336d47a74f8e..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_1<=i_2) /\\ (i_2<=j_1) /\\ (i_0<=9)",
- "pattern": "\\E$i0$i$j$j9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0094,
- "steps": 26 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0101,
- "steps": 26 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
deleted file mode 100644
index 71531584b1405a92d8ecee2ed8fe30b8fd988d3f..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0098,
- "steps": 35 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0048,
- "steps": 35 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
deleted file mode 100644
index 0528b3f539e087d7ffe5b4a4a6ebc4bbce7590eb..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0098,
- "steps": 35 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0048,
- "steps": 35 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
deleted file mode 100644
index aa273fd1e8bb18e8fc52a27351743fe17f464122..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_149) /\\ (i_1<=i_150) /\\ (0<=i_0) /\\ (i_149<=i_0) /\\ (i_150<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.011,
- "steps": 16 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0092,
- "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
deleted file mode 100644
index 3b3491906df49d091101db28c4d58660fed8180a..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0139,
- "steps": 45 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0127,
- "steps": 45 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
deleted file mode 100644
index c31beeea1dd2a6726bca67f972e4aebb07a292c7..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
+++ /dev/null
@@ -1,10 +0,0 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_4) /\\ (i_1<=i_6) /\\ (0<=i_0) /\\ (i_4<=i_0) /\\ (i_6<=i_1) /\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0169,
- "steps": 33 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0081,
- "steps": 33 } ] } } ]