diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index d0d05905e1eccea824ddad15a7e1efc1bad52977..f225a3cb684399e3b2bbab5eee7cc9b7534047bd 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -68,6 +68,8 @@ type convert = {
pool: Lang.F.pool;
polarity: Cvalues.polarity;
in_goal: bool;
+ incomplete_types: (string, Why3.Ty.tysymbol) Hashtbl.t;
+ incomplete_symbols: (string, Why3.Term.lsymbol) Hashtbl.t;
mutable convert_for_export: Lang.F.term Lang.F.Tmap.t;
}
@@ -163,6 +165,8 @@ let empty_cnv ?(polarity=`NoPolarity) ?(in_goal=false) (ctx:context) : convert =
env = ctx.env;
polarity;
in_goal;
+ incomplete_symbols = Hashtbl.create 3;
+ incomplete_types = Hashtbl.create 3;
convert_for_export = Lang.F.Tmap.empty;
}
@@ -252,7 +256,12 @@ let rec of_tau ~cnv (t:Lang.F.tau) =
Some (Why3.Ty.ty_app ts [Why3.Opt.get (of_tau ~cnv k); Why3.Opt.get (of_tau ~cnv v)])
| Data(adt,l) -> begin
let s = name_of_adt adt in
- match Why3.Theory.(ns_find_ts (get_namespace cnv.th) (cut_path s)) with
+ let find s =
+ try Hashtbl.find cnv.incomplete_types s
+ with Not_found ->
+ Why3.Theory.(ns_find_ts (get_namespace cnv.th) (cut_path s))
+ in
+ match find s with
| ts -> Some (Why3.Ty.ty_app ts (List.map (fun e -> Why3.Opt.get (of_tau ~cnv e)) l))
| exception Not_found ->
why3_failure "Can't find type '%s' in why3 namespace" s
@@ -457,7 +466,12 @@ let rec of_term ~cnv expected t : Why3.Term.term =
Why3.Term.t_app ls l r
in
let apply_from_ns s l sort =
- match Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)), expected with
+ let find s =
+ try Hashtbl.find cnv.incomplete_symbols s
+ with Not_found ->
+ Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s))
+ in
+ match find s, expected with
| ls, (Prop | Bool) ->
coerce ~cnv sort expected $
t_app ls l (of_tau cnv sort)
@@ -670,7 +684,7 @@ class visitor (ctx:context) c =
v#add_builtin_lib;
v#vself;
let th = Why3.Theory.close_theory ctx.th in
- if Wp_parameters.has_dkey ProverErgo.dkey_cluster then
+ if Wp_parameters.has_print_generated () then
Log.print_on_output
begin fun fmt ->
Format.fprintf fmt "---------------------------------------------@\n" ;
@@ -784,13 +798,15 @@ class visitor (ctx:context) c =
let decl = Why3.Decl.create_ty_decl id in
ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl;
| Tsum cases ->
- let id = Why3.Ident.id_fresh (Lang.type_id lt) in
+ let name = Lang.type_id lt in
+ let id = Why3.Ident.id_fresh name in
let map i _ = tvar i in
let tv_args = List.mapi map lt.lt_params in
let tys = Why3.Ty.create_tysymbol id tv_args NoDef in
+ let cnv = empty_cnv ctx in
+ Hashtbl.add cnv.incomplete_types name tys ;
let tv_args = List.map Why3.Ty.ty_var tv_args in
let return_ty = Why3.Ty.ty_app tys tv_args in
- let cnv = empty_cnv ctx in
let constr = List.length cases in
let cases = List.map (fun (c,targs) ->
let name = match c with | Lang.CTOR c -> Lang.ctor_id c | _ -> assert false in
@@ -803,13 +819,15 @@ class visitor (ctx:context) c =
let decl = Why3.Decl.create_data_decl [tys,cases] in
ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl;
| Trec fields ->
- let id = Why3.Ident.id_fresh (Lang.type_id lt) in
+ let name = Lang.type_id lt in
+ let id = Why3.Ident.id_fresh name in
let map i _ = tvar i in
let tv_args = List.mapi map lt.lt_params in
let tys = Why3.Ty.create_tysymbol id tv_args NoDef in
+ let cnv = empty_cnv ctx in
+ Hashtbl.add cnv.incomplete_types name tys ;
let tv_args = List.map Why3.Ty.ty_var tv_args in
let return_ty = Why3.Ty.ty_app tys tv_args in
- let cnv = empty_cnv ctx in
let fields,args = List.split @@ List.map (fun (f,ty) ->
let name = Lang.name_of_field f in
let id = Why3.Ident.id_fresh name in
@@ -847,21 +865,23 @@ class visitor (ctx:context) c =
ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl;
end
+ method private make_lemma cnv (l: Definitions.dlemma) =
+ let id = Why3.Ident.id_fresh (Lang.lemma_id l.l_name) in
+ let id = Why3.Decl.create_prsymbol id in
+ List.iter (Lang.F.add_var cnv.pool) l.l_forall;
+ let cnv, vars = Lang.For_export.in_state (mk_binders cnv) l.l_forall in
+ let t = convert cnv Prop (Lang.F.e_prop l.l_lemma) in
+ let triggers = full_triggers l.l_triggers in
+ let triggers = Lang.For_export.in_state (List.map (List.map (of_trigger ~cnv))) triggers in
+ let t = Why3.Term.t_forall_close vars triggers t in
+ id, t
+
method on_dlemma l =
- begin
- let kind = Why3.Decl.(if l.l_assumed then Paxiom else Plemma) in
- let id = Why3.Ident.id_fresh (Lang.lemma_id l.l_name) in
- let id = Why3.Decl.create_prsymbol id in
- let cnv = empty_cnv ctx in
- List.iter (Lang.F.add_var cnv.pool) l.l_forall;
- let cnv, vars = Lang.For_export.in_state (mk_binders cnv) l.l_forall in
- let t = convert cnv Prop (Lang.F.e_prop l.l_lemma) in
- let triggers = full_triggers l.l_triggers in
- let triggers = Lang.For_export.in_state (List.map (List.map (of_trigger ~cnv))) triggers in
- let t = Why3.Term.t_forall_close vars triggers t in
- let decl = Why3.Decl.create_prop_decl kind id t in
- ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl;
- end
+ let kind = Why3.Decl.(if l.l_assumed then Paxiom else Plemma) in
+ let cnv = empty_cnv ctx in
+ let id, t = self#make_lemma cnv l in
+ let decl = Why3.Decl.create_prop_decl kind id t in
+ ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl
method on_dfun d =
Wp_parameters.debug ~dkey:dkey_api "Define %a@." Lang.Fun.pretty d.d_lfun ;
@@ -952,14 +972,18 @@ class visitor (ctx:context) c =
end
| Inductive dl ->
(* create predicate symbol *)
- let id = Why3.Ident.id_fresh (Qed.Export.link_name (lfun_name d.d_lfun)) in
+ let fname = Qed.Export.link_name (lfun_name d.d_lfun) in
+ let id = Why3.Ident.id_fresh fname in
let map e = Why3.Opt.get (of_tau ~cnv (Lang.F.tau_of_var e)) in
let ty_args = List.map map d.d_params in
- let id = Why3.Term.create_lsymbol id ty_args None in
- let decl = Why3.Decl.create_param_decl id in
- ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl ;
- (* register axioms *)
- List.iter (self#on_dlemma) dl
+ let fid = Why3.Term.create_lsymbol id ty_args None in
+ let make_case (l:Definitions.dlemma) =
+ let cnv = empty_cnv ctx in
+ Hashtbl.add cnv.incomplete_symbols fname fid ;
+ self#make_lemma cnv l
+ in
+ let ind_decl = (fid, List.map make_case dl) in
+ ctx.th <- Why3.Theory.add_ind_decl ctx.th Why3.Decl.Ind [ind_decl]
end
end
diff --git a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
index d0bde7870b7a8cade014142226f5f026c223bd3b..ea52c7dcb27540192bf438772975bf952af017e5 100644
--- a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
@@ -4,6 +4,28 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
+---------------------------------------------
+--- Context 'typed_f' Cluster 'Compound'
+---------------------------------------------
+theory Compound
+ (* 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 *)
+
+ function shift_sint32 (p:addr) (k:int) : addr = shift p k
+end
[wp:print-generated]
theory WP
(* use why3.BuiltIn.BuiltIn *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
index d8cb3e9a8d05e830be50775f2197d99d3aaa12af..a1016679f96bf1124f0d163eec275e1e005514b5 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
@@ -3,6 +3,30 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] 3 goals scheduled
+---------------------------------------------
+--- Context 'typed' Cluster 'Compound'
+---------------------------------------------
+theory Compound
+ (* 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 *)
+
+ function shift_sint32 (p:addr) (k:int) : addr = shift p k
+
+ function shiftfield_F1__list_next (p:addr) : addr = shift p 1
+end
[wp:print-generated]
theory WP
(* use why3.BuiltIn.BuiltIn *)
@@ -19,12 +43,10 @@
(* use map.Map *)
- predicate P_is_gcd int int int
-
- axiom Q_gcd_zero : forall n:int. P_is_gcd n 0 n
-
- axiom Q_gcd_succ :
- forall a:int, b:int, d:int. P_is_gcd b (mod a b) d -> P_is_gcd a b d
+ inductive P_is_gcd int int int =
+ | Q_gcd_zero : forall n:int. P_is_gcd n 0 n
+ | Q_gcd_succ :
+ forall a:int, b:int, d:int. P_is_gcd b (mod a b) d -> P_is_gcd a b d
lemma Q_test_no_label :
forall a:int, b:int, d:int. P_is_gcd a b d -> not P_is_gcd b d a
@@ -33,17 +55,15 @@
(* use Compound *)
- predicate P_reachable (int -> int) (addr -> addr) addr addr
-
- axiom Q_root_reachable :
- forall malloc:int -> int, mptr:addr -> addr, root:addr.
- P_reachable malloc mptr root root
-
- axiom 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
+ 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, t2:int -> int, t3:addr -> addr, a:
@@ -65,12 +85,11 @@
(* use map.Map *)
- predicate P_is_gcd1 int int int
-
- axiom Q_gcd_zero1 : forall n:int. P_is_gcd1 n 0 n
-
- axiom Q_gcd_succ1 :
- forall a:int, b:int, d:int. P_is_gcd1 b (mod a b) d -> P_is_gcd1 a b d
+ inductive P_is_gcd1 int int int =
+ | Q_gcd_zero1 : forall n:int. P_is_gcd1 n 0 n
+ | Q_gcd_succ1 :
+ forall a:int, b:int, d:int.
+ P_is_gcd1 b (mod a b) d -> P_is_gcd1 a b d
goal wp_goal :
forall i:int, i1:int, i2:int. P_is_gcd1 i i1 i2 -> not P_is_gcd1 i1 i2 i
@@ -95,29 +114,26 @@
(* use Compound *)
- predicate P_reachable1 (int -> int) (addr -> addr) addr addr
-
- axiom Q_root_reachable1 :
- forall malloc:int -> int, mptr:addr -> addr, root:addr.
- P_reachable1 malloc mptr root root
-
- axiom 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
+ 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_one_label :
forall malloc:int -> int, mptr:addr -> addr, malloc1:int -> int, mptr1:
addr -> addr, l1:addr, l2:addr.
P_reachable1 malloc1 mptr1 l1 l2 -> not P_reachable1 malloc mptr l1 l2
- predicate P_is_gcd2 int int int
-
- axiom Q_gcd_zero2 : forall n:int. P_is_gcd2 n 0 n
-
- axiom Q_gcd_succ2 :
- forall a:int, b:int, d:int. P_is_gcd2 b (mod a b) d -> P_is_gcd2 a b d
+ inductive P_is_gcd2 int int int =
+ | Q_gcd_zero2 : forall n:int. P_is_gcd2 n 0 n
+ | Q_gcd_succ2 :
+ forall a:int, b:int, d:int.
+ P_is_gcd2 b (mod a b) d -> P_is_gcd2 a b d
lemma Q_test_no_label1 :
forall a:int, b:int, d:int. P_is_gcd2 a b d -> not P_is_gcd2 b d a
@@ -142,26 +158,23 @@
i1 < end1 ->
get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
- predicate P_same_elements (addr -> int) (addr -> int) addr addr int int
-
- axiom 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
-
- axiom 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
-
- axiom 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
+ 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, t2:addr -> int, a:addr, a1:addr, i:
diff --git a/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
index fb6e3336de647eebe03fb9c24e275611ec4c23d9..82901ded836c14ba3f2ba30ec3e14fc6463f440b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
@@ -4,6 +4,27 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
+---------------------------------------------
+--- Context 'typed_f' Cluster 'S1_s'
+---------------------------------------------
+theory S1_s
+ (* 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 *)
+
+ type S1_s =
+ | S1_s1 (F1_s_a:int -> int) (F1_s_b:int -> int)
+end
[wp:print-generated]
theory WP
(* use why3.BuiltIn.BuiltIn *)