diff --git a/src/plugins/wp/tests/wp_plugin/abs.driver b/src/plugins/wp/tests/wp_plugin/abs.driver
index 691ecd65e6a56e4e30c9201e273e2bbd6707b9f8..1dec77f8d80595ace2f88e00a464f871953e4a0e 100644
--- a/src/plugins/wp/tests/wp_plugin/abs.driver
+++ b/src/plugins/wp/tests/wp_plugin/abs.driver
@@ -1,5 +1,4 @@
library "abs":
logic integer ABS (integer) = "my_abs" ;
-coq.file := "Abs.v";
why3.file := "abs.why";
diff --git a/src/plugins/wp/tests/wp_plugin/flash.driver b/src/plugins/wp/tests/wp_plugin/flash.driver
index 90ab84348e0d05df1b59ba21f7ba9390c958c512..d4cd3511798bccf8f84f19dd35017f81eb415d30 100644
--- a/src/plugins/wp/tests/wp_plugin/flash.driver
+++ b/src/plugins/wp/tests/wp_plugin/flash.driver
@@ -1,8 +1,8 @@
library INDEX: memory
why3.file += "flash.mlw";
-type index = {coq="dumb"; why3="Flash.t"; } ;
-logic integer INDEX_access( index , addr ) = {coq="dumb"; why3="Flash.get"; } ;
-logic index INDEX_update( index , addr ) = {coq="dumb"; why3="Flash.update"};
+type index = {why3="Flash.t"; } ;
+logic integer INDEX_access( index , addr ) = {why3="Flash.get"; } ;
+logic index INDEX_update( index , addr ) = {why3="Flash.update"};
logic index INDEX_init := "INDEX_init" ;
library RD: INDEX
diff --git a/src/plugins/wp/tests/wp_plugin/inductive.c b/src/plugins/wp/tests/wp_plugin/inductive.c
index fc52022bcb41ba6a0be668ad08de6a8d8a56406a..fb36d5d70c8dae269c984c1ddc9fc335aa4929c4 100644
--- a/src/plugins/wp/tests/wp_plugin/inductive.c
+++ b/src/plugins/wp/tests/wp_plugin/inductive.c
@@ -1,9 +1,9 @@
/* run.config
- OPT: -wp-prover native:coq -wp-gen -wp-msg-key print-generated
+ OPT: -wp-prover why3 -wp-gen -wp-msg-key print-generated
*/
/* run.config_qualif
- OPT: -wp-prover native:coq -wp-coq-script %{dep:@PTEST_DIR@/inductive.script} -wp-timeout 240
+ OPT: -wp-prover coq -wp-coq-script %{dep:@PTEST_DIR@/inductive.script} -wp-timeout 240
*/
typedef struct _list { int element; struct _list* next; } list;
@@ -42,11 +42,11 @@ typedef struct _list { int element; struct _list* next; } list;
}
*/
-/*@ lemma test:
- \forall list *root,*node;
+/*@ lemma test:
+ \forall list *root,*node;
reachable(root,node) ==> ( root == node || (\valid(root) && reachable(root->next, node)) );
*/
-/*@ lemma offset{L1,L2} :
+/*@ lemma offset{L1,L2} :
\forall int *a, *b, integer begin, end, offset;
same_elements{L1,L2}(a+offset,b+offset, begin, end) ==>
same_elements{L1,L2}(a, b, begin+offset, end+offset);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
index 682a46a629d55a852430add96b479063d9d0821c..973a39e45fa5af1ba55ed02d29a1bfe1666b0a7a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
@@ -1,176 +1,149 @@
# frama-c -wp [...]
[kernel] Parsing inductive.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
-[wp:print-generated]
- "WPOUT/typed/Compound.v"
- (* ---------------------------------------------------------- *)
- (* --- Memory Compound Loader --- *)
- (* ---------------------------------------------------------- *)
-
- Require Import ZArith.
- Require Import Reals.
- Require Import BuiltIn.
- Require Import bool.Bool.
- Require Import HighOrd.
- Require Import int.Int.
- Require Import int.Abs.
- Require Import int.ComputerDivision.
- Require Import int.EuclideanDivision.
- Require Import int.ComputerOfEuclideanDivision.
- Require Import real.Real.
- Require Import real.RealInfix.
- Require Import real.FromInt.
- Require Import map.Map.
- Require Import bool.Bool.
- Require Import Qedlib.
- Require Import Qed.
- Require Import Memory.
+---------------------------------------------
+--- Context 'typed' Cluster 'Compound'
+---------------------------------------------
+theory Compound
+ (* use why3.BuiltIn.BuiltIn *)
- Definition shift_sint32 (p : addr) (k : Z) : addr := (shift p k%Z).
-
- Definition shiftfield_F1__list_next (p : addr) : addr := (shift p 1%Z).
-[wp:print-generated]
- "WPOUT/typed/lemma_test_Coq.v"
- (* ---------------------------------------------------------- *)
- (* --- Lemma 'test' --- *)
- (* ---------------------------------------------------------- *)
- Require Import ZArith.
- Require Import Reals.
- Require Import BuiltIn.
- Require Import bool.Bool.
- Require Import HighOrd.
- Require Import int.Int.
- Require Import int.Abs.
- Require Import int.ComputerDivision.
- Require Import int.EuclideanDivision.
- Require Import int.ComputerOfEuclideanDivision.
- Require Import real.Real.
- Require Import real.RealInfix.
- Require Import real.FromInt.
- Require Import map.Map.
- Require Import bool.Bool.
- Require Import Qedlib.
- Require Import Qed.
+ (* use bool.Bool *)
- (* --- Global Definitions --- *)
- Require Import Memory.
+ (* use int.Int *)
- Require Import Compound.
+ (* use int.ComputerDivision *)
- Inductive P_reachable : array Z -> farray addr addr -> addr -> addr ->
- Prop :=
- | Q_root_reachable: forall (t : array Z),
- forall (t_1 : farray addr addr), forall (a : addr),
- (P_reachable t t_1 a a)
- | Q_next_reachable: forall (t : array Z),
- forall (t_1 : farray addr addr), forall (a_1 a : addr),
- ((valid_rw t a_1 2%Z)) ->
- ((P_reachable t t_1 (t_1.[ (shiftfield_F1__list_next a_1) ]) a)) ->
- ((P_reachable t t_1 a_1 a)).
-
- Goal
- forall (t : array Z),
- forall (t_1 : farray addr addr),
- forall (a_1 a : addr),
- ((P_reachable t t_1 a_1 a)) ->
- ((a_1 = a) \/
- (((valid_rw t a_1 2%Z)) /\
- ((P_reachable t t_1 (t_1.[ (shiftfield_F1__list_next a_1) ]) a)))).
-
- Proof.
- ...
- Qed.
-[wp:print-generated]
- "WPOUT/typed/lemma_offset_Coq.v"
- (* ---------------------------------------------------------- *)
- (* --- Lemma 'offset' --- *)
- (* ---------------------------------------------------------- *)
- Require Import ZArith.
- Require Import Reals.
- Require Import BuiltIn.
- Require Import bool.Bool.
- Require Import HighOrd.
- Require Import int.Int.
- Require Import int.Abs.
- Require Import int.ComputerDivision.
- Require Import int.EuclideanDivision.
- Require Import int.ComputerOfEuclideanDivision.
- Require Import real.Real.
- Require Import real.RealInfix.
- Require Import real.FromInt.
- Require Import map.Map.
- Require Import bool.Bool.
- Require Import Qedlib.
- Require Import Qed.
+ (* use real.RealInfix *)
- (* --- Global Definitions --- *)
- Require Import Memory.
+ (* use frama_c_wp.qed.Qed *)
- Require Import Compound.
+ (* use map.Map *)
- Inductive P_reachable : array Z -> farray addr addr -> addr -> addr ->
- Prop :=
- | Q_root_reachable: forall (t : array Z),
- forall (t_1 : farray addr addr), forall (a : addr),
- (P_reachable t t_1 a a)
- | Q_next_reachable: forall (t : array Z),
- forall (t_1 : farray addr addr), forall (a_1 a : addr),
- ((valid_rw t a_1 2%Z)) ->
- ((P_reachable t t_1 (t_1.[ (shiftfield_F1__list_next a_1) ]) a)) ->
- ((P_reachable t t_1 a_1 a)).
+ (* use frama_c_wp.memory.Memory *)
- Hypothesis Q_test: forall (t : array Z), forall (t_1 : farray addr addr),
- forall (a_1 a : addr), ((P_reachable t t_1 a_1 a)) ->
- ((a_1 = a) \/
- (((valid_rw t a_1 2%Z)) /\
- ((P_reachable t t_1 (t_1.[ (shiftfield_F1__list_next a_1) ]) a)))).
+ function shift_sint32 (p:addr) (k:int) : addr = shift p k
- Definition P_same_array (Mint_0 : farray addr Z) (Mint_1 : farray addr Z)
- (a : addr) (b : addr) (begin_0 : Z) (end_0 : Z) : Prop :=
- forall (i : Z), ((begin_0 <= i)%Z) -> ((i < end_0)%Z) ->
- (((Mint_1.[ (shift_sint32 a i%Z) ])
- = (Mint_0.[ (shift_sint32 b i%Z) ]))%Z).
-
- Definition P_swap (Mint_0 : farray addr Z) (Mint_1 : farray addr Z)
- (a : addr) (b : addr) (begin_0 : Z) (i : Z) (j : Z) (end_0 : Z) : Prop :=
- (((Mint_1.[ (shift_sint32 a i%Z) ])
- = (Mint_0.[ (shift_sint32 b j%Z) ]))%Z) /\
- (((Mint_1.[ (shift_sint32 a j%Z) ])
- = (Mint_0.[ (shift_sint32 b i%Z) ]))%Z) /\ ((begin_0 <= i)%Z) /\
- ((i < j)%Z) /\ ((j < end_0)%Z) /\
- (forall (i_1 : Z), ((i_1 <> i)%Z) -> ((i_1 <> j)%Z) ->
- ((begin_0 <= i_1)%Z) -> ((i_1 < end_0)%Z) ->
- (((Mint_1.[ (shift_sint32 a i_1%Z) ])
- = (Mint_0.[ (shift_sint32 b i_1%Z) ]))%Z)).
-
- Inductive P_same_elements : farray addr Z -> farray addr Z -> addr -> addr ->
- Z -> Z -> Prop :=
- | Q_refl: forall (i_1 i : Z), forall (t_1 t : farray addr Z),
- forall (a_1 a : addr), ((P_same_array t_1 t a_1 a i_1%Z i%Z)) ->
- ((P_same_elements t_1 t a_1 a i_1%Z i%Z))
- | Q_swap: forall (i_3 i_2 i_1 i : Z), forall (t_1 t : farray addr Z),
- forall (a_1 a : addr),
- ((P_swap t_1 t a_1 a i_3%Z i_2%Z i_1%Z i%Z)) ->
- ((P_same_elements t_1 t a_1 a i_3%Z i%Z))
- | Q_trans: forall (i_1 i : Z), forall (t_2 t_1 t : farray addr Z),
- forall (a_2 a_1 a : addr),
- ((P_same_elements t_2 t_1 a_1 a i_1%Z i%Z)) ->
- ((P_same_elements t_1 t a_2 a_1 i_1%Z i%Z)) ->
- ((P_same_elements t_2 t a_2 a i_1%Z i%Z)).
-
- Goal
- forall (i_2 i_1 i : Z),
- forall (t_1 t : farray addr Z),
- forall (a_1 a : addr),
- ((P_same_elements t_1 t ((shift_sint32 a_1 i%Z)) ((shift_sint32 a i%Z))
- i_2%Z i_1%Z)) ->
- ((P_same_elements t_1 t a_1 a (i%Z + i_2%Z)%Z (i%Z + i_1%Z)%Z)).
-
- Proof.
- ...
- Qed.
+ function shiftfield_F1__list_next (p:addr) : addr = shift p 1
+end
+[wp:print-generated]
+ theory WP
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ (* use Compound *)
+
+ inductive P_reachable (int -> int) (addr -> addr) addr addr =
+ | Q_root_reachable :
+ forall malloc:int -> int, mptr:addr -> addr, root:addr.
+ P_reachable malloc mptr root root
+ | Q_next_reachable :
+ forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+ valid_rw malloc root 2 ->
+ P_reachable malloc mptr (get mptr (shiftfield_F1__list_next root))
+ node -> P_reachable malloc mptr root node
+
+ goal wp_goal :
+ forall t:int -> int, t1:addr -> addr, a:addr, a1:addr.
+ P_reachable t t1 a a1 ->
+ a1 = a \/
+ valid_rw t a 2 /\
+ P_reachable t t1 (get t1 (shiftfield_F1__list_next a)) a1
+ end
+[wp:print-generated]
+ theory WP1
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ (* use Compound *)
+
+ inductive P_reachable1 (int -> int) (addr -> addr) addr addr =
+ | Q_root_reachable1 :
+ forall malloc:int -> int, mptr:addr -> addr, root:addr.
+ P_reachable1 malloc mptr root root
+ | Q_next_reachable1 :
+ forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+ valid_rw malloc root 2 ->
+ P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root))
+ node -> P_reachable1 malloc mptr root node
+
+ lemma Q_test :
+ forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+ P_reachable1 malloc mptr root node ->
+ root = node \/
+ valid_rw malloc root 2 /\
+ P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root)) node
+
+ predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
+ addr) (begin:int) (end1:int) =
+ forall i:int.
+ begin <= i ->
+ i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
+
+ predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
+ (begin:int) (i:int) (j:int) (end1:int) =
+ ((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
+ get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
+ begin <= i) /\
+ i < j) /\
+ j < end1) /\
+ (forall i1:int.
+ not i1 = i ->
+ not j = i1 ->
+ begin <= i1 ->
+ i1 < end1 ->
+ get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
+
+ inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
+ | Q_refl :
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+ int, end1:int.
+ P_same_array mint mint1 a b begin end1 ->
+ P_same_elements mint mint1 a b begin end1
+ | Q_swap :
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+ int, i:int, j:int, end1:int.
+ P_swap mint mint1 a b begin i j end1 ->
+ P_same_elements mint mint1 a b begin end1
+ | Q_trans :
+ forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
+ addr, b:addr, c:addr, begin:int, end1:int.
+ P_same_elements mint mint1 b c begin end1 ->
+ P_same_elements mint1 mint2 a b begin end1 ->
+ P_same_elements mint mint2 a c begin end1
+
+ goal wp_goal :
+ forall t:addr -> int, t1:addr -> int, a:addr, a1:addr, i:int, i1:int, i2:
+ int.
+ P_same_elements t t1 (shift_sint32 a i2) (shift_sint32 a1 i2) i i1 ->
+ P_same_elements t t1 a a1 (i + i2) (i1 + i2)
+ end
[wp] 2 goals generated
------------------------------------------------------------
Global