[wp] Update Coq qualif tests

src/plugins/wp/tests/wp_plugin/inductive.c

@@ -3,7 +3,7 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-prover coq -wp-coq-script %{dep:@PTEST_DIR@/inductive.script} -wp-timeout 240
+   OPT: -wp-prover coq -wp-timeout 240
 */
 
 typedef struct _list { int element; struct _list* next; } list;

src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle

@@ -2,13 +2,11 @@
 [kernel] Parsing abs.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 1 goal scheduled
-[wp] [Coq] Goal typed_abs_abs_ensures : Saved script
-[wp] [Coq (native)] Goal typed_abs_abs_ensures : Valid
+[wp] [Coq] Goal typed_abs_abs_ensures : Valid
 [wp] Proved goals:    1 / 1
   Qed:             0 
-  Coq (native):    1
+  Coq:             1
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   abs                       -        -        1       100%

src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.session/interactive/abs_ensures.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require HighOrd.
+Require bool.Bool.
+Require int.Int.
+Require int.Abs.
+Require int.ComputerDivision.
+Require real.Real.
+Require real.RealInfix.
+Require real.FromInt.
+Require map.Map.
+
+Parameter eqb:
+  forall {a:Type} {a_WT:WhyType a}, a -> a -> Init.Datatypes.bool.
+
+Axiom eqb1 :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (x:a) (y:a), ((eqb x y) = Init.Datatypes.true) <-> (x = y).
+
+Axiom eqb_false :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (x:a) (y:a), ((eqb x y) = Init.Datatypes.false) <-> ~ (x = y).
+
+Parameter neqb:
+  forall {a:Type} {a_WT:WhyType a}, a -> a -> Init.Datatypes.bool.
+
+Axiom neqb1 :
+  forall {a:Type} {a_WT:WhyType a},
+  forall (x:a) (y:a), ((neqb x y) = Init.Datatypes.true) <-> ~ (x = y).
+
+Parameter zlt: Numbers.BinNums.Z -> Numbers.BinNums.Z -> Init.Datatypes.bool.
+
+Parameter zleq:
+  Numbers.BinNums.Z -> Numbers.BinNums.Z -> Init.Datatypes.bool.
+
+Axiom zlt1 :
+  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+  ((zlt x y) = Init.Datatypes.true) <-> (x < y)%Z.
+
+Axiom zleq1 :
+  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+  ((zleq x y) = Init.Datatypes.true) <-> (x <= y)%Z.
+
+Parameter rlt:
+  Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Init.Datatypes.bool.
+
+Parameter rleq:
+  Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Init.Datatypes.bool.
+
+Axiom rlt1 :
+  forall (x:Reals.Rdefinitions.R) (y:Reals.Rdefinitions.R),
+  ((rlt x y) = Init.Datatypes.true) <-> (x < y)%R.
+
+Axiom rleq1 :
+  forall (x:Reals.Rdefinitions.R) (y:Reals.Rdefinitions.R),
+  ((rleq x y) = Init.Datatypes.true) <-> (x <= y)%R.
+
+(* Why3 assumption *)
+Definition real_of_int (x:Numbers.BinNums.Z) : Reals.Rdefinitions.R :=
+  BuiltIn.IZR x.
+
+Axiom c_euclidian :
+  forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z), ~ (d = 0%Z) ->
+  (n = (((ZArith.BinInt.Z.quot n d) * d)%Z + (ZArith.BinInt.Z.rem n d))%Z).
+
+Axiom cmod_remainder :
+  forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z),
+  ((0%Z <= n)%Z -> (0%Z < d)%Z ->
+   (0%Z <= (ZArith.BinInt.Z.rem n d))%Z /\ ((ZArith.BinInt.Z.rem n d) < d)%Z) /\
+  ((n <= 0%Z)%Z -> (0%Z < d)%Z ->
+   ((-d)%Z < (ZArith.BinInt.Z.rem n d))%Z /\
+   ((ZArith.BinInt.Z.rem n d) <= 0%Z)%Z) /\
+  ((0%Z <= n)%Z -> (d < 0%Z)%Z ->
+   (0%Z <= (ZArith.BinInt.Z.rem n d))%Z /\
+   ((ZArith.BinInt.Z.rem n d) < (-d)%Z)%Z) /\
+  ((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
+   (d < (ZArith.BinInt.Z.rem n d))%Z /\ ((ZArith.BinInt.Z.rem n d) <= 0%Z)%Z).
+
+Axiom cdiv_neutral :
+  forall (a:Numbers.BinNums.Z), ((ZArith.BinInt.Z.quot a 1%Z) = a).
+
+Axiom cdiv_inv :
+  forall (a:Numbers.BinNums.Z), ~ (a = 0%Z) ->
+  ((ZArith.BinInt.Z.quot a a) = 1%Z).
+
+Axiom cdiv_closed_remainder :
+  forall (a:Numbers.BinNums.Z) (b:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
+  (0%Z <= a)%Z -> (0%Z <= b)%Z ->
+  (0%Z <= (b - a)%Z)%Z /\ ((b - a)%Z < n)%Z ->
+  ((ZArith.BinInt.Z.rem a n) = (ZArith.BinInt.Z.rem b n)) -> (a = b).
+
+(* Why3 assumption *)
+Definition is_bool (x:Numbers.BinNums.Z) : Prop := (x = 0%Z) \/ (x = 1%Z).
+
+(* Why3 assumption *)
+Definition is_uint8 (x:Numbers.BinNums.Z) : Prop :=
+  (0%Z <= x)%Z /\ (x < 256%Z)%Z.
+
+(* Why3 assumption *)
+Definition is_sint8 (x:Numbers.BinNums.Z) : Prop :=
+  ((-128%Z)%Z <= x)%Z /\ (x < 128%Z)%Z.
+
+(* Why3 assumption *)
+Definition is_uint16 (x:Numbers.BinNums.Z) : Prop :=
+  (0%Z <= x)%Z /\ (x < 65536%Z)%Z.
+
+(* Why3 assumption *)
+Definition is_sint16 (x:Numbers.BinNums.Z) : Prop :=
+  ((-32768%Z)%Z <= x)%Z /\ (x < 32768%Z)%Z.
+
+(* Why3 assumption *)
+Definition is_uint32 (x:Numbers.BinNums.Z) : Prop :=
+  (0%Z <= x)%Z /\ (x < 4294967296%Z)%Z.
+
+(* Why3 assumption *)
+Definition is_sint32 (x:Numbers.BinNums.Z) : Prop :=
+  ((-2147483648%Z)%Z <= x)%Z /\ (x < 2147483648%Z)%Z.
+
+(* Why3 assumption *)
+Definition is_uint64 (x:Numbers.BinNums.Z) : Prop :=
+  (0%Z <= x)%Z /\ (x < 18446744073709551616%Z)%Z.
+
+(* Why3 assumption *)
+Definition is_sint64 (x:Numbers.BinNums.Z) : Prop :=
+  ((-9223372036854775808%Z)%Z <= x)%Z /\ (x < 9223372036854775808%Z)%Z.
+
+Axiom is_bool0 : is_bool 0%Z.
+
+Axiom is_bool1 : is_bool 1%Z.
+
+Parameter to_bool: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Axiom to_bool'def :
+  forall (x:Numbers.BinNums.Z),
+  ((x = 0%Z) -> ((to_bool x) = 0%Z)) /\ (~ (x = 0%Z) -> ((to_bool x) = 1%Z)).
+
+Parameter to_uint8: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Parameter to_sint8: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Parameter to_uint16: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Parameter to_sint16: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Parameter to_uint32: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Parameter to_sint32: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Parameter to_uint64: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Parameter to_sint64: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Parameter two_power_abs: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Axiom two_power_abs_is_positive :
+  forall (n:Numbers.BinNums.Z), (0%Z < (two_power_abs n))%Z.
+
+Axiom two_power_abs_plus_pos :
+  forall (n:Numbers.BinNums.Z) (m:Numbers.BinNums.Z), (0%Z <= n)%Z ->
+  (0%Z <= m)%Z ->
+  ((two_power_abs (n + m)%Z) = ((two_power_abs n) * (two_power_abs m))%Z).
+
+Axiom two_power_abs_plus_one :
+  forall (n:Numbers.BinNums.Z), (0%Z <= n)%Z ->
+  ((two_power_abs (n + 1%Z)%Z) = (2%Z * (two_power_abs n))%Z).
+
+(* Why3 assumption *)
+Definition is_uint (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z) : Prop :=
+  (0%Z <= x)%Z /\ (x < (two_power_abs n))%Z.
+
+(* Why3 assumption *)
+Definition is_sint (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z) : Prop :=
+  ((-(two_power_abs n))%Z <= x)%Z /\ (x < (two_power_abs n))%Z.
+
+Parameter to_uint:
+  Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Parameter to_sint:
+  Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Axiom is_to_uint :
+  forall (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z), is_uint n (to_uint n x).
+
+Axiom is_to_sint :
+  forall (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z), is_sint n (to_sint n x).
+
+Axiom is_to_uint8 : forall (x:Numbers.BinNums.Z), is_uint8 (to_uint8 x).
+
+Axiom is_to_sint8 : forall (x:Numbers.BinNums.Z), is_sint8 (to_sint8 x).
+
+Axiom is_to_uint16 : forall (x:Numbers.BinNums.Z), is_uint16 (to_uint16 x).
+
+Axiom is_to_sint16 : forall (x:Numbers.BinNums.Z), is_sint16 (to_sint16 x).
+
+Axiom is_to_uint32 : forall (x:Numbers.BinNums.Z), is_uint32 (to_uint32 x).
+
+Axiom is_to_sint32 : forall (x:Numbers.BinNums.Z), is_sint32 (to_sint32 x).
+
+Axiom is_to_uint64 : forall (x:Numbers.BinNums.Z), is_uint64 (to_uint64 x).
+
+Axiom is_to_sint64 : forall (x:Numbers.BinNums.Z), is_sint64 (to_sint64 x).
+
+Axiom id_uint :
+  forall (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z),
+  is_uint n x <-> ((to_uint n x) = x).
+
+Axiom id_sint :
+  forall (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z),
+  is_sint n x <-> ((to_sint n x) = x).
+
+Axiom id_uint8 :
+  forall (x:Numbers.BinNums.Z), is_uint8 x -> ((to_uint8 x) = x).
+
+Axiom id_sint8 :
+  forall (x:Numbers.BinNums.Z), is_sint8 x -> ((to_sint8 x) = x).
+
+Axiom id_uint16 :
+  forall (x:Numbers.BinNums.Z), is_uint16 x -> ((to_uint16 x) = x).
+
+Axiom id_sint16 :
+  forall (x:Numbers.BinNums.Z), is_sint16 x -> ((to_sint16 x) = x).
+
+Axiom id_uint32 :
+  forall (x:Numbers.BinNums.Z), is_uint32 x -> ((to_uint32 x) = x).
+
+Axiom id_sint32 :
+  forall (x:Numbers.BinNums.Z), is_sint32 x -> ((to_sint32 x) = x).
+
+Axiom id_uint64 :
+  forall (x:Numbers.BinNums.Z), is_uint64 x -> ((to_uint64 x) = x).
+
+Axiom id_sint64 :
+  forall (x:Numbers.BinNums.Z), is_sint64 x -> ((to_sint64 x) = x).
+
+Axiom proj_uint :
+  forall (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z),
+  ((to_uint n (to_uint n x)) = (to_uint n x)).
+
+Axiom proj_sint :
+  forall (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z),
+  ((to_sint n (to_sint n x)) = (to_sint n x)).
+
+Axiom proj_uint8 :
+  forall (x:Numbers.BinNums.Z), ((to_uint8 (to_uint8 x)) = (to_uint8 x)).
+
+Axiom proj_sint8 :
+  forall (x:Numbers.BinNums.Z), ((to_sint8 (to_sint8 x)) = (to_sint8 x)).
+
+Axiom proj_uint16 :
+  forall (x:Numbers.BinNums.Z), ((to_uint16 (to_uint16 x)) = (to_uint16 x)).
+
+Axiom proj_sint16 :
+  forall (x:Numbers.BinNums.Z), ((to_sint16 (to_sint16 x)) = (to_sint16 x)).
+
+Axiom proj_uint32 :
+  forall (x:Numbers.BinNums.Z), ((to_uint32 (to_uint32 x)) = (to_uint32 x)).
+
+Axiom proj_sint32 :
+  forall (x:Numbers.BinNums.Z), ((to_sint32 (to_sint32 x)) = (to_sint32 x)).
+
+Axiom proj_uint64 :
+  forall (x:Numbers.BinNums.Z), ((to_uint64 (to_uint64 x)) = (to_uint64 x)).
+
+Axiom proj_sint64 :
+  forall (x:Numbers.BinNums.Z), ((to_sint64 (to_sint64 x)) = (to_sint64 x)).
+
+Axiom proj_su :
+  forall (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z),
+  ((to_sint n (to_uint n x)) = (to_uint n x)).
+
+Axiom incl_su :
+  forall (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z), is_uint n x ->
+  is_sint n x.
+
+Axiom proj_su_uint :
+  forall (n:Numbers.BinNums.Z) (m:Numbers.BinNums.Z) (x:Numbers.BinNums.Z),
+  (0%Z <= n)%Z -> (0%Z <= m)%Z ->
+  ((to_sint (m + n)%Z (to_uint n x)) = (to_uint n x)).
+
+Axiom proj_su_sint :
+  forall (n:Numbers.BinNums.Z) (m:Numbers.BinNums.Z) (x:Numbers.BinNums.Z),
+  (0%Z <= n)%Z -> (0%Z <= m)%Z ->
+  ((to_sint n (to_uint (m + (n + 1%Z)%Z)%Z x)) = (to_sint n x)).
+
+Axiom proj_int8 :
+  forall (x:Numbers.BinNums.Z), ((to_sint8 (to_uint8 x)) = (to_sint8 x)).
+
+Axiom proj_int16 :
+  forall (x:Numbers.BinNums.Z), ((to_sint16 (to_uint16 x)) = (to_sint16 x)).
+
+Axiom proj_int32 :
+  forall (x:Numbers.BinNums.Z), ((to_sint32 (to_uint32 x)) = (to_sint32 x)).
+
+Axiom proj_int64 :
+  forall (x:Numbers.BinNums.Z), ((to_sint64 (to_uint64 x)) = (to_sint64 x)).
+
+Axiom proj_us_uint :
+  forall (n:Numbers.BinNums.Z) (m:Numbers.BinNums.Z) (x:Numbers.BinNums.Z),
+  (0%Z <= n)%Z -> (0%Z <= m)%Z ->
+  ((to_uint (n + 1%Z)%Z (to_sint (m + n)%Z x)) = (to_uint (n + 1%Z)%Z x)).
+
+Axiom incl_uint :
+  forall (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z) (i:Numbers.BinNums.Z),
+  (0%Z <= n)%Z -> (0%Z <= i)%Z -> is_uint n x -> is_uint (n + i)%Z x.
+
+Axiom incl_sint :
+  forall (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z) (i:Numbers.BinNums.Z),
+  (0%Z <= n)%Z -> (0%Z <= i)%Z -> is_sint n x -> is_sint (n + i)%Z x.
+
+Axiom incl_int :
+  forall (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z) (i:Numbers.BinNums.Z),
+  (0%Z <= n)%Z -> (0%Z <= i)%Z -> is_uint n x -> is_sint (n + i)%Z x.
+
+Parameter my_abs: Numbers.BinNums.Z -> Numbers.BinNums.Z.
+
+Axiom abs_pos :
+  forall (x:Numbers.BinNums.Z), (0%Z <= x)%Z -> ((my_abs x) = x).
+
+Axiom abs_neg :
+  forall (x:Numbers.BinNums.Z), (x <= 0%Z)%Z -> ((my_abs x) = (-x)%Z).
+
+(* Why3 goal *)
+Theorem wp_goal :
+  forall (i:Numbers.BinNums.Z) (i1:Numbers.BinNums.Z), is_sint32 i1 ->
+  is_sint32 i ->
+  (i1 < 0%Z)%Z /\ ((i + i1)%Z = 0%Z) \/ ~ (i1 < 0%Z)%Z /\ (i1 = i) ->
+  ((my_abs i1) = i).
+Proof.
+  Require Import Psatz.
+
+  intros i n Hn Hi H ; intros.
+  inversion_clear H as [ C1 | C2 ].
+  + inversion_clear C1 as [ Nn Hin ].
+    assert (Heq: i = (-n)%Z) by lia.
+    rewrite Heq ; apply abs_neg ; lia.
+  + inversion_clear C2 as [ Pn Hin ] ; subst.
+    apply abs_pos ; lia.
+Qed.
+

src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle

@@ -5,12 +5,10 @@
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 1 goal scheduled
-[wp] [Coq] Goal typed_output_ensures_KO : Default tactic
-[wp] [Coq (native)] Goal typed_output_ensures_KO : Unsuccess
+[wp] [Coq] Goal typed_output_ensures_KO : Unsuccess
 [wp] Proved goals:    0 / 1
-  Coq (native):    0  (unsuccess: 1)
+  Coq:             0  (unsuccess: 1)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   output                    -        -        1       0.0%