Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 9467fe73 authored by MARCHE Claude's avatar MARCHE Claude

Desactivation des warnings 41 44 et 45 car trop nombreux

parent 8e1cfbcf
......@@ -63,8 +63,8 @@ HACHA = @HACHA@
#PSVIEWER = @PSVIEWER@
#PDFVIEWER = @PDFVIEWER@
OFLAGS = -w Aer-29 -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w Aer-29 -dtypes -g -I lib/why3 $(INCLUDES)
OFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
OLINKFLAGS = -linkall $(EXTCMXA)
BLINKFLAGS = -linkall $(EXTCMA)
......
......@@ -4,7 +4,7 @@ let lt_nat (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
Int__Int.infix_lseq (Why3__BuiltIn.int_constant "0") y &&
Int__Int.infix_ls x y
let rec lex (x: (Why3__BuiltIn.int * Why3__BuiltIn.int)) (x1:
let lex (x: (Why3__BuiltIn.int * Why3__BuiltIn.int)) (x1:
(Why3__BuiltIn.int * Why3__BuiltIn.int)) : bool =
let (fst1, snd1) = x in
let (fst2, snd2) = x1 in
......
......@@ -26,7 +26,7 @@ type prelude = string list
type prelude_map = prelude Mid.t
type blacklist = string list
type 'a pp = formatter -> 'a -> unit
type 'a pp = Pp.formatter -> 'a -> unit
type printer_args = {
env : Env.env;
......
......@@ -105,8 +105,8 @@ let gen_decl_l add fn =
in
fold_l fn
let decl = gen_decl add_decl
let decl_l = gen_decl_l add_decl
let decl = gen_decl Task.add_decl
let decl_l = gen_decl_l Task.add_decl
let tdecl = gen_decl add_tdecl
let tdecl_l = gen_decl_l add_tdecl
......@@ -124,8 +124,8 @@ let gen_goal_l add fn = function
List.map (List.fold_left add prev) (apply_to_goal fn d)
| _ -> assert false
let goal = gen_goal add_decl
let goal_l = gen_goal_l add_decl
let goal = gen_goal Task.add_decl
let goal_l = gen_goal_l Task.add_decl
let tgoal = gen_goal add_tdecl
let tgoal_l = gen_goal_l add_tdecl
......@@ -134,10 +134,10 @@ let rewriteTF fnT fnF = rewrite (TermTF.t_select fnT fnF)
let gen_add_decl add decls = store (function
| Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
add_decl (List.fold_left add prev decls) d
Task.add_decl (List.fold_left add prev decls) d
| _ -> assert false)
let add_decls = gen_add_decl add_decl
let add_decls = gen_add_decl Task.add_decl
let add_tdecls = gen_add_decl add_tdecl
(** dependent transformations *)
......
......@@ -126,7 +126,7 @@ and dpattern_node =
| Por of dpattern * dpattern
| Pas of dpattern * ident
let create_user_id { id = x ; id_lab = ll ; id_loc = loc } =
let create_user_id { id = x ; id_lab = ll ; Ptree.id_loc = loc } =
let get_labels (ll,p) = function
| Lstr l -> Slab.add l ll, p
| Lpos p -> ll, Some p
......@@ -170,7 +170,7 @@ and dterm_node =
| Tif of dfmla * dterm * dterm
| Tlet of dterm * ident * dterm
| Tmatch of dterm * (dpattern * dterm) list
| Tnamed of label * dterm
| Tnamed of Ptree.label * dterm
| Teps of ident * dty * dfmla
and dfmla =
......@@ -183,7 +183,7 @@ and dfmla =
| Fif of dfmla * dfmla * dfmla
| Flet of dterm * ident * dfmla
| Fmatch of dterm * (dpattern * dfmla) list
| Fnamed of label * dfmla
| Fnamed of Ptree.label * dfmla
| Fvar of term
and dtrigger =
......
......@@ -517,7 +517,7 @@ let print_goal info fmt g =
let print_task args ?old:_ fmt task =
forget_all ident_printer;
let info = get_info args.env task in
print_prelude fmt (List.append args.prelude ["$MaxExtraPrecision = 256;
print_prelude fmt (List.append args.prelude ["$MaxExtraPrecision = 256;\
ClearAll[vcWhy,varsWhy,resWhy];"]);
print_th_prelude task fmt args.th_prelude;
let params,funs,preds,eqs,hyps,goal,types =
......
......@@ -112,11 +112,13 @@ struct
Mutex.lock queue_lock
done
(* dead code
let yield () =
Thread.yield ();
Mutex.lock queue_lock;
treat_result ();
Mutex.unlock queue_lock
*)
(** Wait for the last remaining tasks *)
let wait_remaining_task () =
......
......@@ -15,7 +15,6 @@ open Theory
open Task
open Trans
open Driver
open Call_provers
module BenchUtil : sig
val maximum_running_proofs: int ref
......
......@@ -15,8 +15,10 @@ open Why3
open Stdlib
(* dead code
type id_tool = (string * string)
type id_prob = (string * string * string)
*)
type benchrc = { tools : tool list Mstr.t;
probs : prob list Mstr.t;
......
......@@ -28,32 +28,33 @@ let print_footer fmt () =
let style_css fname =
let c = open_out fname in
output_string c
"
.why3doc a:visited {color : #416DFF; text-decoration : none; }
.why3doc a:link {color : #416DFF; text-decoration : none;}
.why3doc a:hover {color : Red; text-decoration : none; background-color: #5FFF88}
.why3doc a:active {color : Red; text-decoration : underline; }
.why3doc .comment { color : #990000 }
.why3doc .keyword1 { color : purple; font-weight : bold }
.why3doc .keyword2 { color : blue; font-weight : bold }
.why3doc .superscript { font-size : 4 }
.why3doc .subscript { font-size : 4 }
.why3doc .warning { color : Red ; font-weight : bold }
.why3doc .info { margin-left : 3em; margin-right : 3em }
.why3doc .code { color : #465F91 ; }
.why3doc h1 { font-size : 20pt ; border: 1px solid #000000; margin-top: 10px; margin-bottom: 10px;text-align: center; background-color: #90BDFF ;padding: 10px; }
.why3doc h2 { font-size : 18pt ; border: 1px solid #000000; margin-top: 8px; margin-bottom: 8px;text-align: left; background-color: #90DDFF ;padding: 8px; }
.why3doc h3 { font-size : 16pt ; border: 1px solid #000000; margin-top: 6px; margin-bottom: 6px;text-align: left; background-color: #90EDFF ;padding: 6px; }
.why3doc h4 { font-size : 14pt ; border: 1px solid #000000; margin-top: 4px; margin-bottom: 4px;text-align: left; background-color: #90FDFF ;padding: 4px; }
.why3doc h5 { font-size : 12pt ; border: 1px solid #000000; margin-top: 2px; margin-bottom: 2px;text-align: left; background-color: #90BDFF ; padding: 2px; }
.why3doc h6 { font-size : 10pt ; border: 1px solid #000000; margin-top: 0px; margin-bottom: 0px;text-align: left; background-color: #90BDFF ; padding: 0px; }
.why3doc .typetable { border-style : hidden }
.why3doc .indextable { border-style : hidden }
.why3doc .paramstable { border-style : hidden ; padding: 5pt 5pt}
.why3doc body { background-color : White }
.why3doc tr { background-color : White }
.why3doc td.typefieldcomment { background-color : #FFFFFF }
.why3doc pre { margin-top: 1px ; margin-bottom: 2px; }
.why3doc div.sig_block {margin-left: 2em}";
"\
.why3doc a:visited {color : #416DFF; text-decoration : none; }\
.why3doc a:link {color : #416DFF; text-decoration : none;}\
.why3doc a:hover {color : Red; text-decoration : none; background-color: #5FFF88}\
.why3doc a:active {color : Red; text-decoration : underline; }\
.why3doc .comment { color : #990000 }\
.why3doc .keyword1 { color : purple; font-weight : bold }\
.why3doc .keyword2 { color : blue; font-weight : bold }\
.why3doc .superscript { font-size : 4 }\
.why3doc .subscript { font-size : 4 }\
.why3doc .warning { color : Red ; font-weight : bold }\
.why3doc .info { margin-left : 3em; margin-right : 3em }\
.why3doc .code { color : #465F91 ; }\
.why3doc h1 { font-size : 20pt ; border: 1px solid #000000; margin-top: 10px; margin-bottom: 10px;text-align: center; background-color: #90BDFF ;padding: 10px; }\
.why3doc h2 { font-size : 18pt ; border: 1px solid #000000; margin-top: 8px; margin-bottom: 8px;text-align: left; background-color: #90DDFF ;padding: 8px; }\
.why3doc h3 { font-size : 16pt ; border: 1px solid #000000; margin-top: 6px; margin-bottom: 6px;text-align: left; background-color: #90EDFF ;padding: 6px; }\
.why3doc h4 { font-size : 14pt ; border: 1px solid #000000; margin-top: 4px; margin-bottom: 4px;text-align: left; background-color: #90FDFF ;padding: 4px; }\
.why3doc h5 { font-size : 12pt ; border: 1px solid #000000; margin-top: 2px; margin-bottom: 2px;text-align: left; background-color: #90BDFF ; padding: 2px; }\
.why3doc h6 { font-size : 10pt ; border: 1px solid #000000; margin-top: 0px; margin-bottom: 0px;text-align: left; background-color: #90BDFF ; padding: 0px; }\
.why3doc .typetable { border-style : hidden }\
.why3doc .indextable { border-style : hidden }\
.why3doc .paramstable { border-style : hidden ; padding: 5pt 5pt}\
.why3doc body { background-color : White }\
.why3doc tr { background-color : White }\
.why3doc td.typefieldcomment { background-color : #FFFFFF }\
.why3doc pre { margin-top: 1px ; margin-bottom: 2px; }\
.why3doc div.sig_block {margin-left: 2em}\
";
close_out c
......@@ -233,17 +233,17 @@ let rec num_lines acc tr =
print_file) s.session_files
let context : context = "<!DOCTYPE html
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
<title>Why3 session of %s</title>
</head>
<body>
%a
</body>
</html>
let context : context = "<!DOCTYPE html\
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\
<html xmlns=\"http://www.w3.org/1999/xhtml\">\
<head>\
<title>Why3 session of %s</title>\
</head>\
<body>\
%a\
</body>\
</html>\
"
let run_one = run_file context print_session
......@@ -301,17 +301,17 @@ struct
print_file) s.session_files
let context : context = "<!DOCTYPE html
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
<title>Why3 session of %s</title>
</head>
<body>
%a
</body>
</html>
let context : context = "<!DOCTYPE html\
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\
<html xmlns=\"http://www.w3.org/1999/xhtml\">\
<head>\
<title>Why3 session of %s</title>\
</head>\
<body>\
%a\
</body>\
</html>\
"
let run_one = run_file context print_session
......@@ -435,71 +435,71 @@ onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
session.session_files in
fprintf fmt
"<a href='#' onclick=\"$('#%s_session').jstree('open_all');\">
expand all
</a> <a href='#' onclick=\"$('#%s_session').jstree('close_all');\">
close all
</a>
<div id=\"%s_session\" class=\"session\">
%a
</div>
<script type=\"text/javascript\" class=\"source\">
$(function () {
$(\"#%s_session\").jstree({
\"types\" : {
\"types\" : {
\"file\" : {
\"icon\" : { \"image\" : \"images/folder16.png\"},
},
\"theory\" : {
\"icon\" : { \"image\" : \"images/folder16.png\"},
},
\"goal\" : {
\"icon\" : { \"image\" : \"images/file16.png\"},
},
\"prover\" : {
\"icon\" : { \"image\" : \"images/wizard16.png\"},
},
\"transf\" : {
\"icon\" : { \"image\" : \"images/configure16.png\"},
},
}
},
\"plugins\" : [\"themes\",\"html_data\",\"types\"]
});
});
</script>
"<a href='#' onclick=\"$('#%s_session').jstree('open_all');\">\
expand all\
</a> <a href='#' onclick=\"$('#%s_session').jstree('close_all');\">\
close all\
</a>\
<div id=\"%s_session\" class=\"session\">\
%a\
</div>\
<script type=\"text/javascript\" class=\"source\">\
$(function () {\
$(\"#%s_session\").jstree({\
\"types\" : {\
\"types\" : {\
\"file\" : {\
\"icon\" : { \"image\" : \"images/folder16.png\"},\
},\
\"theory\" : {\
\"icon\" : { \"image\" : \"images/folder16.png\"},\
},\
\"goal\" : {\
\"icon\" : { \"image\" : \"images/file16.png\"},\
},\
\"prover\" : {\
\"icon\" : { \"image\" : \"images/wizard16.png\"},\
},\
\"transf\" : {\
\"icon\" : { \"image\" : \"images/configure16.png\"},\
},\
}\
},\
\"plugins\" : [\"themes\",\"html_data\",\"types\"]\
});\
});\
</script>\
"
name name name print_session_aux name name
let context : context = "<!DOCTYPE html
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\" />
<title>Why3 session of %s</title>
<link rel=\"stylesheet\" type=\"text/css\"
href=\"javascript/session.css\" />
<script type=\"text/javascript\" src=\"javascript/jquery.js\"></script>
let context : context = "<!DOCTYPE html\
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\
<html xmlns=\"http://www.w3.org/1999/xhtml\">\
<head>\
<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\" />\
<title>Why3 session of %s</title>\
<link rel=\"stylesheet\" type=\"text/css\"\
href=\"javascript/session.css\" />\
<script type=\"text/javascript\" src=\"javascript/jquery.js\"></script>\
<script type=\"text/javascript\" src=\"javascript/jquery.jstree.js\">\
</script>
</script>\
<script type=\"text/javascript\" src=\"javascript/session.js\">\
</script>
</head>
<body>
%a
<iframe src=\"\" id='edited'>
<p>Your browser does not support iframes.</p>
</iframe>
<script type=\"text/javascript\" class=\"source\">
$(function () {
$('#edited').hide()
})
</script>
</body>
</html>
</script>\
</head>\
<body>\
%a\
<iframe src=\"\" id='edited'>\
<p>Your browser does not support iframes.</p>\
</iframe>\
<script type=\"text/javascript\" class=\"source\">\
$(function () {\
$('#edited').hide()\
})\
</script>\
</body>\
</html>\
"
let run_files config =
......
......@@ -81,24 +81,24 @@ let opt_verbosity = ref Vnormal
let spec =
[
"--edit", Arg.Symbol (["all";"diff";"none"],set_edit_opt),
" set when the user can edit an interactive proof:
- all: edit all the proofs not proved valid
- diff: edit all the proofs that have a different result
" set when the user can edit an interactive proof:\
- all: edit all the proofs not proved valid\
- diff: edit all the proofs that have a different result\
- none: never ask (default)";
"-e", Arg.Unit (fun () -> set_edit_opt "all"),
" same as --edit all";
"--modif", Arg.Symbol (["all";"obsolete";"none"],set_save_opt),
" set when modification of proofs are saved:
- all: apply all modifications
- obsolete: modify only the proofs that were obsolete or are new
" set when modification of proofs are saved:\
- all: apply all modifications\
- obsolete: modify only the proofs that were obsolete or are new\
- none: modify nothing (default)";
"-m", Arg.Unit (fun () -> set_save_opt "all"),
" same as --modif all";
"--out-of-sync", Arg.Symbol (["none";"success";"usual"],set_outofsync_opt),
" set what to do with sessions which are out-of-sync with the \
original file or with why3:
- none: don't open sessions which are out-of-sync
- success: save them only if all the goals are proved at the end (default)
original file or with why3:\
- none: don't open sessions which are out-of-sync\
- success: save them only if all the goals are proved at the end (default)\
- usual: don't consider them specially";
"--quiet",Arg.Unit (fun () -> opt_verbosity := Vquiet),
" remove the progression";
......@@ -295,7 +295,7 @@ let run_one sched env config filters interactive_provers fname =
else
edit_proof a old_res new_res
and edit_proof a old_res new_res =
printf "@[<hov 2>From@ file@ %s:@\n
printf "@[<hov 2>From@ file@ %s:@\n\
Do@ you@ want@ to@ edit@ %a@ that@ fail@ with@ the@ result@ \
%a@\nPreviously@ %a.@]@."
fname print_external_proof a C.print_prover_result new_res
......
......@@ -10,7 +10,6 @@
(********************************************************************)
open Format
open Stdlib
open Term
......
......@@ -462,7 +462,8 @@ let add_lemma_label ~top id = function
| Gnone -> id, false
| Gghost -> id, true
| Glemma when not top ->
errorm ~loc:id.id_loc "lemma functions are only allowed at toplevel"
errorm ~loc:id. Ptree.id_loc
"lemma functions are only allowed at toplevel"
| Glemma -> { id with id_lab = Lstr Mlw_wp.lemma_label :: id.id_lab }, true
let de_unit ~loc = hidden_ls ~loc Mlw_expr.fs_void
......@@ -1273,9 +1274,9 @@ and expr_desc lenv loc de = match de.de_desc with
e_abstract e1 spec
| DEassert (ak, f) ->
let ak = match ak with
| Ptree.Aassert -> Aassert
| Ptree.Aassume -> Aassume
| Ptree.Acheck -> Acheck in
| Ptree.Aassert -> Mlw_expr.Aassert
| Ptree.Aassume -> Mlw_expr.Aassume
| Ptree.Acheck -> Mlw_expr.Acheck in
e_assert ak (create_assert lenv f)
| DEabsurd ->
e_absurd (ity_of_dity (snd de.de_type))
......@@ -1335,8 +1336,8 @@ and expr_desc lenv loc de = match de.de_desc with
let inv = create_pre lenv inv in
let e1 = expr lenv de1 in
let dir = match dir with
| Ptree.To -> To
| Ptree.Downto -> DownTo in
| Ptree.To -> Mlw_expr.To
| Ptree.Downto -> Mlw_expr.DownTo in
e_for pv efrom dir eto inv e1
and expr_rec lenv dfdl =
......@@ -1368,7 +1369,7 @@ and expr_rec lenv dfdl =
let fdl = create_rec_defn (List.map step3 fdl) in
let step4 fd (id,_,_,bl,(de,dsp)) =
Loc.try4 ~loc:de.de_loc check_lambda_effect lenv fd bl dsp;
Loc.try2 ~loc:id.id_loc check_user_ps true fd.fun_ps in
Loc.try2 ~loc:id.Ptree.id_loc check_user_ps true fd.fun_ps in
List.iter2 step4 fdl dfdl;
fdl
......@@ -1561,7 +1562,7 @@ let add_types ~wp uc tdl =
with Not_found ->
let d = Mstr.find x def in
let add_tv acc id =
let e = Loc.Located (id.id_loc, DuplicateTypeVar id.id) in
let e = Loc.Located (id.Ptree.id_loc, DuplicateTypeVar id.id) in
let tv = Typing.create_user_tv id.id in
Mstr.add_new e id.id tv acc in
let vars = List.fold_left add_tv Mstr.empty d.td_params in
......
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