Skip to content

GitLab

why3
why3
Commit d1a5ec78 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

silence Z warnings and fix a couple of nasty bugs in the meantime

parent 1a166dae
Hide whitespace changes
Inline Side-by-side
Showing with 56 additions and 67 deletions
Makefile.in
View file @ d1a5ec78
......@@ -59,8 +59,8 @@ OCAMLVERSION = @OCAMLVERSION@
#PSVIEWER = @PSVIEWER@
#PDFVIEWER = @PDFVIEWER@
BFLAGS = -w Ae -warn-error Z -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Ae -warn-error Z -dtypes -I src $(INCLUDES)
BFLAGS = -w Ae -dtypes -g -I src $(INCLUDES)
OFLAGS = -w Ae -dtypes -I src $(INCLUDES)
# external libraries common to all binaries
......
src/coq-plugin/whytac.ml
View file @ d1a5ec78
......@@ -271,7 +271,7 @@ and tr_global_ts env r =
with Not_found ->
add_global global_ts r None;
match r with
| VarRef id ->
| VarRef _id ->
assert false (*TODO*)
| ConstructRef _ ->
assert false
......
src/core/decl.ml
View file @ d1a5ec78
......@@ -58,16 +58,8 @@ let make_ls_defn ls vl = e_apply (make_fs_defn ls vl) (make_ps_defn ls vl)
let open_ls_defn (_,f) =
let vl, ef = f_open_forall f in
match ef.f_node with
| Fapp (s, [t1; t2]) when s == ps_equ ->
begin match t1.t_node with
| Tapp (fs, _) -> vl, Term t2
| _ -> assert false
end
| Fbinop (Fiff, f1, f2) ->
begin match f1.f_node with
| Fapp (ps, _) -> vl, Fmla f2
| _ -> assert false
end
| Fapp (_, [_; t2]) -> vl, Term t2
| Fbinop (_, _, f2) -> vl, Fmla f2
| _ -> assert false
let open_fs_defn ld = let vl,e = open_ls_defn ld in
......@@ -137,7 +129,7 @@ module Hsdecl = Hashcons.Make (struct
| None, None -> true
| _ -> false
let eq_iax (pr1,fr1) (pr2,fr2) = pr1 == pr1 && fr1 == fr2
let eq_iax (pr1,fr1) (pr2,fr2) = pr1 == pr2 && fr1 == fr2
let eq_ind (ps1,al1) (ps2,al2) = ps1 == ps2 && list_all2 eq_iax al1 al2
......@@ -507,7 +499,7 @@ let find_prop kn pr =
| Dind dl ->
let test (_,l) = List.mem_assq pr l in
List.assq pr (snd (List.find test dl))
| Dprop (_,pr,f) -> f
| Dprop (_,_,f) -> f
| _ -> assert false
exception NonExhaustiveExpr of (pattern list * expr)
......
src/core/term.ml
View file @ d1a5ec78
......@@ -294,10 +294,7 @@ module Hsterm = Hashcons.Make (struct
| Tvar v1, Tvar v2 -> v1 == v2
| Tconst c1, Tconst c2 -> c1 = c2
| Tapp (s1, l1), Tapp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2
(* Claude: en voila un beau bug
j'espere que cela convaincra les developpeurs
de Why3 de compiler avec l'option -w Z !!! *)
| Tif (f1, t1, e1), Tif (f2, t2, e2) -> f1 == f2 && t1 == t2 && e2 == e2
| Tif (f1, t1, e1), Tif (f2, t2, e2) -> f1 == f2 && t1 == t2 && e1 == e2
| Tlet (t1, b1), Tlet (t2, b2) -> t1 == t2 && t_eq_bound b1 b2
| Tcase (tl1, bl1), Tcase (tl2, bl2) ->
list_all2 (==) tl1 tl2 && list_all2 t_eq_branch bl1 bl2
......@@ -536,22 +533,22 @@ let brlvl fn lvl acc (_, nv, t) = fn (lvl + nv) acc t
let t_fold_unsafe fnT fnF lvl acc t = match t.t_node with
| Tbvar n when n >= lvl -> raise UnboundIndex
| Tbvar _ | Tvar _ | Tconst _ -> acc
| Tapp (f, tl) -> List.fold_left (fnT lvl) acc tl
| Tapp (_, tl) -> List.fold_left (fnT lvl) acc tl
| Tif (f, t1, t2) -> fnT lvl (fnT lvl (fnF lvl acc f) t1) t2
| Tlet (t1, (u, t2)) -> fnT (lvl + 1) (fnT lvl acc t1) t2
| Tlet (t1, (_, t2)) -> fnT (lvl + 1) (fnT lvl acc t1) t2
| Tcase (tl, bl) ->
List.fold_left (brlvl fnT lvl) (List.fold_left (fnT lvl) acc tl) bl
| Teps (u, f) -> fnF (lvl + 1) acc f
| Teps (_, f) -> fnF (lvl + 1) acc f
let f_fold_unsafe fnT fnF lvl acc f = match f.f_node with
| Fapp (p, tl) -> List.fold_left (fnT lvl) acc tl
| Fquant (q, (vl, nv, tl, f1)) -> let lvl = lvl + nv in
| Fapp (_, tl) -> List.fold_left (fnT lvl) acc tl
| Fquant (_, (_, nv, tl, f1)) -> let lvl = lvl + nv in
tr_fold (fnT lvl) (fnF lvl) (fnF lvl acc f1) tl
| Fbinop (op, f1, f2) -> fnF lvl (fnF lvl acc f1) f2
| Fbinop (_, f1, f2) -> fnF lvl (fnF lvl acc f1) f2
| Fnot f1 -> fnF lvl acc f1
| Ftrue | Ffalse -> acc
| Fif (f1, f2, f3) -> fnF lvl (fnF lvl (fnF lvl acc f1) f2) f3
| Flet (t, (u, f1)) -> fnF (lvl + 1) (fnT lvl acc t) f1
| Flet (t, (_, f1)) -> fnF (lvl + 1) (fnT lvl acc t) f1
| Fcase (tl, bl) ->
List.fold_left (brlvl fnF lvl) (List.fold_left (fnT lvl) acc tl) bl
......@@ -732,10 +729,10 @@ and f_s_fold fnT fnL acc f =
let fn_v acc u = ty_s_fold fnT acc u.vs_ty in
match f.f_node with
| Fapp (p, tl) -> List.fold_left fn_t (fnL acc p) tl
| Fquant (q, (vl,_,tl,f1)) ->
| Fquant (_, (vl,_,tl,f1)) ->
let acc = List.fold_left fn_v acc vl in
fn_f (tr_fold fn_t fn_f acc tl) f1
| Fbinop (op, f1, f2) -> fn_f (fn_f acc f1) f2
| Fbinop (_, f1, f2) -> fn_f (fn_f acc f1) f2
| Fnot f1 -> fn_f acc f1
| Ftrue | Ffalse -> acc
| Fif (f1, f2, f3) -> fn_f (fn_f (fn_f acc f1) f2) f3
......@@ -964,7 +961,7 @@ let f_branch fn acc b = let _,f = f_open_branch b in fn acc f
let t_fold fnT fnF acc t = match t.t_node with
| Tbvar _ -> raise UnboundIndex
| Tvar _ | Tconst _ -> acc
| Tapp (f, tl) -> List.fold_left fnT acc tl
| Tapp (_, tl) -> List.fold_left fnT acc tl
| Tif (f, t1, t2) -> fnT (fnT (fnF acc f) t1) t2
| Tlet (t1, b) -> let _,t2 = t_open_bound b in fnT (fnT acc t1) t2
| Tcase (tl, bl) ->
......@@ -972,10 +969,10 @@ let t_fold fnT fnF acc t = match t.t_node with
| Teps b -> let _,f = f_open_bound b in fnF acc f
let f_fold fnT fnF acc f = match f.f_node with
| Fapp (p, tl) -> List.fold_left fnT acc tl
| Fquant (q, b) -> let vl, tl, f1 = f_open_quant b in
| Fapp (_, tl) -> List.fold_left fnT acc tl
| Fquant (_, b) -> let _, tl, f1 = f_open_quant b in
tr_fold fnT fnF (fnF acc f1) tl
| Fbinop (op, f1, f2) -> fnF (fnF acc f1) f2
| Fbinop (_, f1, f2) -> fnF (fnF acc f1) f2
| Fnot f1 -> fnF acc f1
| Ftrue | Ffalse -> acc
| Fif (f1, f2, f3) -> fnF (fnF (fnF acc f1) f2) f3
......@@ -1043,8 +1040,8 @@ let f_subst_single v t1 f = f_v_map (eq_vs v t1) f
(* set of free variables *)
let t_freevars s t = t_v_fold (fun s u -> Svs.add u s) Svs.empty t
let f_freevars s f = f_v_fold (fun s u -> Svs.add u s) Svs.empty f
let t_freevars s t = t_v_fold (fun s u -> Svs.add u s) s t
let f_freevars s f = f_v_fold (fun s u -> Svs.add u s) s f
(* equality modulo alpha *)
......@@ -1063,15 +1060,15 @@ let rec t_equal_alpha t1 t2 =
| Tif (f1, t1, e1), Tif (f2, t2, e2) ->
f_equal_alpha f1 f2 && t_equal_alpha t1 t2 && t_equal_alpha e1 e2
| Tlet (t1, tb1), Tlet (t2, tb2) ->
let v1, b1 = tb1 in
let v2, b2 = tb2 in
let _, b1 = tb1 in
let _, b2 = tb2 in
t_equal_alpha t1 t2 && t_equal_alpha b1 b2
| Tcase (tl1, bl1), Tcase (tl2, bl2) ->
list_all2 t_equal_alpha tl1 tl2 &&
list_all2 t_equal_branch_alpha bl1 bl2
| Teps fb1, Teps fb2 ->
let v1, f1 = fb1 in
let v2, f2 = fb2 in
let _, f1 = fb1 in
let _, f2 = fb2 in
f_equal_alpha f1 f2
| _ -> false
......@@ -1092,8 +1089,8 @@ and f_equal_alpha f1 f2 =
| Fif (f1, g1, h1), Fif (f2, g2, h2) ->
f_equal_alpha f1 f2 && f_equal_alpha g1 g2 && f_equal_alpha h1 h2
| Flet (t1, fb1), Flet (t2, fb2) ->
let v1, f1 = fb1 in
let v2, f2 = fb2 in
let _, f1 = fb1 in
let _, f2 = fb2 in
t_equal_alpha t1 t2 && f_equal_alpha f1 f2
| Fcase (tl1, bl1), Fcase (tl2, bl2) ->
list_all2 t_equal_alpha tl1 tl2 &&
......@@ -1145,16 +1142,16 @@ let rec t_match s t1 t2 =
| Tif (f1, t1, e1), Tif (f2, t2, e2) ->
t_match (t_match (f_match s f1 f2) t1 t2) e1 e2
| Tlet (t1, tb1), Tlet (t2, tb2) ->
let v1, b1 = tb1 in
let v2, b2 = tb2 in
let _, b1 = tb1 in
let _, b2 = tb2 in
t_match (t_match s t1 t2) b1 b2
| Tcase (tl1, bl1), Tcase (tl2, bl2) ->
(try List.fold_left2 t_match_branch
(List.fold_left2 t_match s tl1 tl2) bl1 bl2
with Invalid_argument _ -> raise NoMatch)
| Teps fb1, Teps fb2 ->
let v1, f1 = fb1 in
let v2, f2 = fb2 in
let _, f1 = fb1 in
let _, f2 = fb2 in
f_match s f1 f2
| _ -> raise NoMatch
......@@ -1175,8 +1172,8 @@ and f_match s f1 f2 =
| Fif (f1, g1, h1), Fif (f2, g2, h2) ->
f_match (f_match (f_match s f1 f2) g1 g2) h1 h2
| Flet (t1, fb1), Flet (t2, fb2) ->
let v1, f1 = fb1 in
let v2, f2 = fb2 in
let _, f1 = fb1 in
let _, f2 = fb2 in
f_match (t_match s t1 t2) f1 f2
| Fcase (tl1, bl1), Fcase (tl2, bl2) ->
(try List.fold_left2 f_match_branch
......
src/driver/call_provers.ml
View file @ d1a5ec78
......@@ -171,7 +171,7 @@ let treat_result pr (t,c,outerr) =
here or in the use of why_cpulimit *)
Timeout
| Unix.WSTOPPED _ | Unix.WSIGNALED _ -> HighFailure
| Unix.WEXITED c ->
| Unix.WEXITED _ ->
let rec greps res = function
| [] -> HighFailure
| (r,pa)::l ->
......
src/driver/driver.ml
View file @ d1a5ec78
......@@ -289,7 +289,7 @@ let load_rules env (premap,tmap) {thr_name = loc,qualid; thr_rules = trl} =
with Not_found -> errorm ~loc "Unknown proposition %s"
(string_of_qualid qualid q)
end
| Rprelude (loc,s) ->
| Rprelude (_loc,s) ->
let l =
try Mid.find th.th_name premap
with Not_found -> []
......@@ -435,7 +435,7 @@ let file_printer =
[]
let call_prover_on_file ?debug ?timeout drv filename =
Call_provers.on_file drv.drv_prover filename
Call_provers.on_file ?debug ?timeout drv.drv_prover filename
let call_prover_on_formatter ?debug ?timeout ?filename drv ib =
Call_provers.on_formatter ?debug ?timeout ?filename drv.drv_prover ib
let call_prover_on_buffer ?debug ?timeout ?filename drv ib =
......
src/main.ml
View file @ d1a5ec78
......@@ -197,7 +197,7 @@ let print_th_namespace fmt th =
let fname_printer = ref (Ident.create_ident_printer [])
let do_task env drv fname tname (th : Why.Theory.theory) (task : Task.task) =
let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) =
if !opt_prove then begin
let res = Driver.call_prover ~debug:!opt_debug ?timeout drv task in
printf "%s %s %s : %a@." fname tname
......
src/parser/typing.ml
View file @ d1a5ec78
......@@ -217,7 +217,7 @@ let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)
let specialize_lsymbol p uc =
let s = find_lsymbol p uc in
s, specialize_lsymbol (qloc p) s
s, specialize_lsymbol ~loc:(qloc p) s
let specialize_fsymbol p uc =
let s, (tl, ty) = specialize_lsymbol p uc in
......
src/printer/alt_ergo.ml
View file @ d1a5ec78
......@@ -171,7 +171,7 @@ let print_type_decl drv fmt = function
let ac_th = ["algebra";"AC"]
let print_logic_decl drv task fmt (ls,ld) =
let print_logic_decl drv _task fmt (ls,ld) =
match drv ls.ls_name with
| Driver.Remove | Driver.Syntax _ -> false
| Driver.Tag s ->
......
src/printer/smt.ml
View file @ d1a5ec78
......@@ -39,7 +39,7 @@ let ident_printer =
let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
let print_tvsymbols fmt id = assert false
let print_tvsymbols _fmt _id = assert false
let forget_var v = forget_id ident_printer v.vs_name
......@@ -117,7 +117,7 @@ let rec print_fmla drv fmt f = match f.f_node with
end
| Fquant (q, fq) ->
let q = match q with Fforall -> "forall" | Fexists -> "exists" in
let vl, tl, f = f_open_quant fq in
let vl, _tl, f = f_open_quant fq in
(* TODO trigger *)
let rec forall fmt = function
| [] -> print_fmla drv fmt f
......@@ -172,10 +172,10 @@ let print_type_decl drv fmt = function
| _, Talgebraic _ ->
assert false
let print_logic_decl drv task fmt (ls,ld) =
let print_logic_decl drv _task fmt (ls,ld) =
match drv ls.ls_name with
| Driver.Remove | Driver.Syntax _ -> false
| Driver.Tag s ->
| Driver.Tag _s ->
begin match ld with
| None ->
begin match ls.ls_value with
......@@ -189,7 +189,7 @@ let print_logic_decl drv task fmt (ls,ld) =
(print_list space (print_type drv)) ls.ls_args
(print_type drv) value
end
| Some ld -> assert false (* Dealt in Encoding *)
| Some _ -> assert false (* Dealt in Encoding *)
end;
true
......@@ -201,7 +201,7 @@ let print_decl drv task fmt d = match d.d_node with
| Dind _ -> assert false (* TODO *)
| Dprop (Paxiom, pr, _) when
drv pr.pr_name = Driver.Remove -> false
| Dprop (Paxiom, pr, f) ->
| Dprop (Paxiom, _pr, f) ->
fprintf fmt "@[<hov 2>:assumption@ %a@]@\n"
(print_fmla drv) f; true
| Dprop (Pgoal, pr, f) ->
......
src/programs/pgm_typing.ml
View file @ d1a5ec78
......@@ -151,7 +151,7 @@ and expr_desc env loc = function
let e2 = dexpr env e2 in
expected_type e2 env.ty_bool;
DElazy (op, e1, e2), env.ty_bool
| Pgm_ptree.Ematch (el, bl) ->
| Pgm_ptree.Ematch (_el, _bl) ->
assert false (*TODO*)
| Pgm_ptree.Eskip ->
DEskip, env.ty_unit
......@@ -222,7 +222,7 @@ and expr_desc env denv = function
| DElabel (s, e1) ->
Elabel (s, expr env e1)
let code uc id e =
let code uc _id e =
let env = create_denv uc in
let e = dexpr env e in
ignore (expr Mstr.empty e)
......
src/transform/encoding_decorate.ml
View file @ d1a5ec78
......@@ -230,7 +230,7 @@ and rewrite_fmla tenv tvar vsvar f =
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args in
f_app p tl
| Fquant (q, b) -> let vl, tl, f1 = f_open_quant b in
| Fquant (q, b) -> let vl, _tl, f1 = f_open_quant b in
let conv_vs (vsvar,acc) vs =
let tres,vsres =
let ty_res = conv_ty_pos tenv vs.vs_ty in
......@@ -268,7 +268,7 @@ let decl (tenv:tenv) d =
type which are not in recursive bloc")
| Dlogic l ->
let fn = function
| ls, Some _ -> assert false (* TODO or not
| _ls, Some _ -> assert false (* TODO or not
(remove_logic_definition*)
| ls, None ->
try
......@@ -279,7 +279,7 @@ let decl (tenv:tenv) d =
Hls.add tenv.trans_lsymbol ls ls_conv;
ls_conv,None in
[create_logic_decl (List.map fn l)]
| Dind l -> failwith ("Encoding_decorate : I can't work on inductive")
| Dind _ -> failwith ("Encoding_decorate : I can't work on inductive")
(* let fn (pr,f) = pr, fnF f in *)
(* let fn (ps,l) = ps, List.map fn l in *)
(* [create_ind_decl (List.map fn l)] *)
......
src/transform/inlining.ml
View file @ d1a5ec78
......@@ -56,7 +56,7 @@ and replacep env f =
match f.f_node with
| Fapp (ps,tl) ->
begin try
let (vs,t) = Mls.find ps env.ps in
let (vs,f) = Mls.find ps env.ps in
let m = List.fold_left2 (fun acc x y -> Mvs.add x y acc)
Mvs.empty vs tl in
f_subst m f
......@@ -101,7 +101,7 @@ let fold isnotinlinedt isnotinlinedf d (env, task) =
let vs,e = open_ls_defn ld in
let e = e_map (replacet env) (replacep env) e in
make_ls_defn ls vs e) dl))
| Dtype dl -> env,add_decl task d
| Dtype _ -> env,add_decl task d
| Dprop (k,pr,f) ->
env,add_decl task (create_prop_decl k pr (replacep env f))
......@@ -121,14 +121,14 @@ let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
let trivial = t
~isnotinlinedt:(fun m -> match m.t_node with
| Tconst _ | Tvar _ -> false
| Tapp (ls,tl) when List.for_all
| Tapp (_,tl) when List.for_all
(fun m -> match m.t_node with
| Tvar _ -> true
| _ -> false) tl -> false
| _ -> true )
~isnotinlinedf:(fun m -> match m.f_node with
| Ftrue | Ffalse -> false
| Fapp (ls,tl) when List.for_all
| Fapp (_,tl) when List.for_all
(fun m -> match m.t_node with
| Tvar _ -> true
| _ -> false) tl -> false
......
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