1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2025 -- Inria - CNRS - Paris-Saclay University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(********************************************************************)
(*******************
This file builds some MLW modules, using parse trees instead of direct
API calls
******************)
(* BEGIN{buildenv} *)
open Why3
let config : Whyconf.config = Whyconf.init_config None
let main : Whyconf.main = Whyconf.get_main config
let env : Env.env = Env.create_env (Whyconf.loadpath main)
(* END{buildenv} *)
(*
declaration of
BEGIN{source2}
let f2 () : int
requires { true }
ensures { result >= 0 }
= let x = ref 42 in !x
END{source2}
*)
(* BEGIN{code2_import} *)
let int_module : Pmodule.pmodule =
Pmodule.read_module env ["int"] "Int"
let ge_int : Term.lsymbol =
Theory.ns_find_ls int_module.Pmodule.mod_theory.Theory.th_export
[Ident.op_infix ">="]
let ref_module : Pmodule.pmodule =
Pmodule.read_module env ["ref"] "Ref"
let ref_type : Ity.itysymbol =
Pmodule.ns_find_its ref_module.Pmodule.mod_export ["ref"]
(* the "ref" function *)
let ref_fun : Expr.rsymbol =
Pmodule.ns_find_rs ref_module.Pmodule.mod_export ["ref"]
(* the "!" function *)
let get_fun : Expr.rsymbol =
Pmodule.ns_find_rs ref_module.Pmodule.mod_export [Ident.op_prefix "!"]
(* END{code2_import} *)
(* BEGIN{code2} *)
let d2 =
let id = Ident.id_fresh "f" in
let post =
let result =
Term.create_vsymbol (Ident.id_fresh "result") Ty.ty_int
in
let post = Term.ps_app ge_int [Term.t_var result; Term.t_nat_const 0] in
Ity.create_post result post
in
let body =
(* building expression "ref 42" *)
let e =
let c0 = Expr.e_const (Constant.int_const_of_int 42) Ity.ity_int in
let refzero_type = Ity.ity_app ref_type [Ity.ity_int] [] in
Expr.e_app ref_fun [c0] [] refzero_type
in
(* building the first part of the let x = ref 42 *)
let id_x = Ident.id_fresh "x" in
let letdef, var_x = Expr.let_var id_x e in
(* building expression "!x" *)
let bang_x = Expr.e_app get_fun [Expr.e_var var_x] [] Ity.ity_int in
(* the complete body *)
Expr.e_let letdef bang_x
in
let arg_unit =
let unit = Ident.id_fresh "unit" in
Ity.create_pvsymbol unit Ity.ity_unit
in
let def,_rs = Expr.let_sym id
(Expr.c_fun [arg_unit] [] [post] Ity.Mxs.empty Ity.Mpv.empty body) in
Pdecl.create_let_decl def
(* END{code2} *)
(* BEGIN{createmodule} *)
let mod2 =
let uc : Pmodule.pmodule_uc =
Pmodule.create_module env (Ident.id_fresh "MyModule")
in
let uc = Pmodule.use_export uc int_module in
let uc = Pmodule.use_export uc ref_module in
let uc = Pmodule.add_pdecl ~vc:true uc d2 in
Pmodule.close_module uc
(* END{createmodule} *)
(* Checking the VCs *)
(* BEGIN{checkingvcs} *)
let my_tasks : Task.task list =
Task.split_theory mod2.Pmodule.mod_theory None None
open Format
let () =
printf "Tasks are:@.";
let _ =
List.fold_left
(fun i t -> printf "@[<v 0>== Task %d ==@\n@\n%a@]@." i Pretty.print_task t; i+1)
1 my_tasks
in ()
let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers config
let limits =
Call_provers.{empty_limits with
limit_time = Whyconf.timelimit main;
limit_mem = Whyconf.memlimit main }
let alt_ergo : Whyconf.config_prover =
let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
(* all provers that have the name "Alt-Ergo" *)
let provers = Whyconf.filter_provers config fp in
if Whyconf.Mprover.is_empty provers then begin
eprintf "Prover Alt-Ergo not installed or not configured@.";
exit 1
end else
snd (Whyconf.Mprover.max_binding provers)
let alt_ergo_driver : Driver.driver =
try
Driver.load_driver_for_prover main env alt_ergo
with e ->
eprintf "Failed to load driver for alt-ergo: %a@."
Exn_printer.exn_printer e;
exit 1
let () =
let _ =
List.fold_left
(fun i t ->
let r =
Call_provers.wait_on_call
(Driver.prove_task
~limits
~config:main
~command:alt_ergo.Whyconf.command
alt_ergo_driver
t)
in
printf "@[On task %d, alt-ergo answers %a@."
i (Call_provers.print_prover_result ?json:None) r;
i+1
)
1 my_tasks
in ()
(* END{checkingvcs} *)
(*
Local Variables:
compile-command: "ocaml -I ../../lib/why3 unix.cma nums.cma str.cma dynlink.cma -I `ocamlfind query menhirLib` menhirLib.cmo -I `ocamlfind query camlzip` zip.cma ../../lib/why3/why3.cma mlw_tree.ml"
End:
*)
|
