Commit 589e548c authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[WP] Use driver to tell about Why3 WP-specific libraries

parent ceed3aba
...@@ -34,6 +34,11 @@ let option_import = LogicBuiltins.create_option ...@@ -34,6 +34,11 @@ let option_import = LogicBuiltins.create_option
(fun ~driver_dir:_ x -> x) (fun ~driver_dir:_ x -> x)
"why3" "import" "why3" "import"
let option_qual =
LogicBuiltins.create_option
(fun ~driver_dir:_ x -> x)
"why3" "qualifier"
let why3_failure msg = let why3_failure msg =
Pretty_utils.ksfprintf failwith msg Pretty_utils.ksfprintf failwith msg
...@@ -227,6 +232,16 @@ let regexp_dot = Str.regexp_string "." ...@@ -227,6 +232,16 @@ let regexp_dot = Str.regexp_string "."
let cut_path s = Str.split_delim regexp_dot s let cut_path s = Str.split_delim regexp_dot s
let wp_why3_lib library =
match LogicBuiltins.get_option option_qual ~library with
| [] -> [library]
| [ lib ] -> Str.split_delim regexp_dot lib
| l ->
let pp_sep fmt () = Format.pp_print_string fmt ", " in
Wp_parameters.fatal
"too many bindings for WP-specific Why3 theory file %s:@\n%a"
library Format.(pp_print_list ~pp_sep pp_print_string) l
(* conversion *) (* conversion *)
let rec of_tau ~cnv (t:Lang.F.tau) = let rec of_tau ~cnv (t:Lang.F.tau) =
...@@ -364,13 +379,13 @@ let rec of_term ~cnv expected t : Why3.Term.term = ...@@ -364,13 +379,13 @@ let rec of_term ~cnv expected t : Why3.Term.term =
a b a b
| Leq (a,b), _, Bool -> | Leq (a,b), _, Bool ->
int_or_real ~cnv int_or_real ~cnv
~fint:["frama_c_wp"; "qed"] ~lint:"Qed" ~pint:["zleq"] ~fint:(wp_why3_lib "qed") ~lint:"Qed" ~pint:["zleq"]
~freal:["frama_c_wp"; "qed"] ~lreal:"Qed" ~preal:["rleq"] ~freal:(wp_why3_lib "qed") ~lreal:"Qed" ~preal:["rleq"]
a b a b
| Lt (a,b), _, Bool -> | Lt (a,b), _, Bool ->
int_or_real ~cnv int_or_real ~cnv
~fint:["frama_c_wp"; "qed"] ~lint:"Qed" ~pint:["zlt"] ~fint:(wp_why3_lib "qed") ~lint:"Qed" ~pint:["zlt"]
~freal:["frama_c_wp"; "qed"] ~lreal:"Qed" ~preal:["rlt"] ~freal:(wp_why3_lib "qed") ~lreal:"Qed" ~preal:["rlt"]
a b a b
| And l, _, Bool -> | And l, _, Bool ->
t_app_fold ~f:["bool"] ~l:"Bool" ~p:["andb"] ~cnv expected l t_app_fold ~f:["bool"] ~l:"Bool" ~p:["andb"] ~cnv expected l
...@@ -420,9 +435,9 @@ let rec of_term ~cnv expected t : Why3.Term.term = ...@@ -420,9 +435,9 @@ let rec of_term ~cnv expected t : Why3.Term.term =
| _ -> Why3.Term.t_neq (of_term' cnv a) (of_term' cnv b) | _ -> Why3.Term.t_neq (of_term' cnv a) (of_term' cnv b)
end end
| Eq (a,b), _, Bool -> | Eq (a,b), _, Bool ->
t_app ~cnv ~f:["frama_c_wp"; "qed"] ~l:"Qed" ~p:["eqb"] [of_term' cnv a; of_term' cnv b] t_app ~cnv ~f:(wp_why3_lib "qed") ~l:"Qed" ~p:["eqb"] [of_term' cnv a; of_term' cnv b]
| Neq (a,b), _, Bool -> | Neq (a,b), _, Bool ->
t_app ~cnv ~f:["frama_c_wp"; "qed"] ~l:"Qed" ~p:["neqb"] [of_term' cnv a; of_term' cnv b] t_app ~cnv ~f:(wp_why3_lib "qed") ~l:"Qed" ~p:["neqb"] [of_term' cnv a; of_term' cnv b]
| If(a,b,c), _, _ -> | If(a,b,c), _, _ ->
let cnv' = {cnv with polarity = `NoPolarity} in let cnv' = {cnv with polarity = `NoPolarity} in
Why3.Term.t_if (of_term cnv' Prop a) (of_term cnv expected b) (of_term cnv expected c) Why3.Term.t_if (of_term cnv' Prop a) (of_term cnv expected b) (of_term cnv expected c)
......
...@@ -38,6 +38,7 @@ coq.file += "coqwp/Qedlib.v"; ...@@ -38,6 +38,7 @@ coq.file += "coqwp/Qedlib.v";
coq.file += "coqwp/Qed.v"; coq.file += "coqwp/Qed.v";
why3.import += "int.Abs:IAbs"; why3.import += "int.Abs:IAbs";
why3.import += "frama_c_wp.qed.Qed"; why3.import += "frama_c_wp.qed.Qed";
why3.qualifier := "frama_c_wp.qed";
altergo.file += "ergo/int.Int.mlw"; altergo.file += "ergo/int.Int.mlw";
altergo.file += "ergo/int.Abs.mlw"; altergo.file += "ergo/int.Abs.mlw";
altergo.file += "ergo/int.ComputerDivision.mlw"; altergo.file += "ergo/int.ComputerDivision.mlw";
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment