diff --git a/src/bench/bench.ml b/src/bench/bench.ml
index a1782f6ad68e314680dd882e5eb579db4bea0cdc..16d4b70b7eaec8e64ea49f3502b26549ef2be458 100644
--- a/src/bench/bench.ml
+++ b/src/bench/bench.ml
@@ -432,6 +432,7 @@ let empty_tool_res =
{tr with timeout = add_nb_avg tr.timeout time}
| Db.Done Call_provers.Invalid ->
{tr with invalid = add_nb_avg tr.invalid time}
+ | Db.Done Call_provers.OutOfMemory
| Db.Undone | Db.Done (Call_provers.Unknown _) ->
{tr with unknown = add_nb_avg tr.unknown time}
| Db.Done (Call_provers.Failure _)
diff --git a/src/bench/db.ml b/src/bench/db.ml
index d963524001744de1472e2698b7c6009b05ea6ae1..53a6bf7bbf97b111fa2bd84f7beafa56e929b2f8 100644
--- a/src/bench/db.ml
+++ b/src/bench/db.ml
@@ -477,6 +477,7 @@ let int64_from_status = function
| Done (Call_provers.Failure _) -> 4L
| Done Call_provers.Invalid -> 5L
| Done Call_provers.HighFailure -> 6L
+ | Done Call_provers.OutOfMemory -> 7L
let status_array = [|
Undone;
@@ -485,7 +486,9 @@ let status_array = [|
Done (Call_provers.Unknown "");
Done (Call_provers.Failure "");
Done Call_provers.Invalid;
- Done Call_provers.HighFailure; |]
+ Done Call_provers.HighFailure;
+ Done Call_provers.OutOfMemory;
+|]
let status_from_int64 i =
try
diff --git a/src/why3session/why3session_html.ml b/src/why3session/why3session_html.ml
index ebc2374c18d066de796e22a418a0e55cb30f8ba7..88a6edfe843a6cea0b12221a79e765757d393663 100644
--- a/src/why3session/why3session_html.ml
+++ b/src/why3session/why3session_html.ml
@@ -36,7 +36,7 @@ let set_opt_style = function
| "simple" -> opt_style := SimpleTree
| "jstree" -> opt_style := Jstree
| "table" -> opt_style := Table
- | _ ->
+ | _ ->
eprintf "Unknown html style, ignored@."
let () = set_opt_style default_style
@@ -120,9 +120,9 @@ struct
let print_prover = Whyconf.print_prover
- let color_of_status ?(dark=false) fmt b =
- fprintf fmt "%s" (if b then
- if dark then "008000" else "C0FFC0"
+ let color_of_status ?(dark=false) fmt b =
+ fprintf fmt "%s" (if b then
+ if dark then "008000" else "C0FFC0"
else "FF0000")
let print_results fmt provers proofs =
@@ -147,9 +147,9 @@ let print_results fmt provers proofs =
| Call_provers.Unknown _ ->
fprintf fmt "FF8000\">%.2f" res.Call_provers.pr_time
| Call_provers.Failure _ ->
- fprintf fmt "FF8000\">Failure "
- | Call_provers.HighFailure _ ->
- fprintf fmt "FF8000\">High Failure "
+ fprintf fmt "FF8000\">Failure"
+ | Call_provers.HighFailure ->
+ fprintf fmt "FF8000\">High Failure"
end
| S.Undone _ -> fprintf fmt "E0E0E0\">Undone"
| S.InternalFailure _ -> fprintf fmt "E0E0E0\">Internal Failure"
@@ -159,16 +159,16 @@ let print_results fmt provers proofs =
let rec num_lines acc tr =
List.fold_left
- (fun acc g -> 1 +
- PHstr.fold (fun _ tr acc -> 1 + num_lines acc tr)
+ (fun acc g -> 1 +
+ PHstr.fold (fun _ tr acc -> 1 + num_lines acc tr)
g.goal_transformations acc)
acc tr.transf_goals
let rec print_transf fmt depth max_depth provers tr =
fprintf fmt "<tr>";
for i=1 to 0 (* depth-1 *) do fprintf fmt "<td></td>" done;
- fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
- (color_of_status ~dark:false) tr.S.transf_verified
+ fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
+ (color_of_status ~dark:false) tr.S.transf_verified
(max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt " " done; *)
fprintf fmt "%s</td>" tr.transf_name ;
@@ -187,7 +187,7 @@ let rec num_lines acc tr =
and print_goal fmt is_first depth max_depth provers g =
if not is_first then fprintf fmt "<tr>";
(* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "<td></td>" done; *)
- fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
+ fprintf fmt "<td bgcolor=\"#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) g.S.goal_verified (max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt " " done; *)
fprintf fmt "%s</td>" (S.goal_expl g);
@@ -208,7 +208,7 @@ let rec num_lines acc tr =
in
let provers = List.sort Whyconf.Prover.compare provers in
let name = th.S.theory_name.Ident.id_string in
- fprintf fmt "<h2><font color=\"#%a\">Theory \"%s\": %s</font></h2>@\n"
+ fprintf fmt "<h2><font color=\"#%a\">Theory \"%s\": %s</font></h2>@\n"
(color_of_status ~dark:true) th.S.theory_verified
name (if th.S.theory_verified then "fully verified" else "not fully verified")
;
diff --git a/src/why3session/why3session_latex.ml b/src/why3session/why3session_latex.ml
index ece8709f3c775cd62ed04c688b8be4b31d78b03a..5d8537300003961be002494d3f4b2471fcbb68a0 100644
--- a/src/why3session/why3session_latex.ml
+++ b/src/why3session/why3session_latex.ml
@@ -45,7 +45,7 @@ let spec =
("-o",
Arg.Set_string opt_output_dir,
"<dir> where to produce LaTeX files (default: session dir)") ::
- ("-e",
+ ("-e",
Arg.String add_element,
"<path> produce a table for the element denoted by <path>") ::
("-longtable",
@@ -142,7 +142,8 @@ let print_result_prov proofs prov fmt=
| Call_provers.OutOfMemory -> fprintf fmt "& \\outofmemory "
| Call_provers.Unknown _ -> fprintf fmt "& \\unknown "
| Call_provers.Failure _ -> fprintf fmt "& \\failure "
- | Call_provers.HighFailure _ -> fprintf fmt "& \\highfailure "
+ | Call_provers.HighFailure -> fprintf fmt "& \\highfailure "
+
end
| Session.InternalFailure _ -> fprintf fmt "& Internal Failure"
| Session.Undone _ -> fprintf fmt "& Undone"
@@ -389,7 +390,7 @@ let element_latex_stat_theory th n table dir e =
| g :: r ->
try
let goals =
- List.map (fun g -> (g.S.goal_name.Ident.id_string,g))
+ List.map (fun g -> (g.S.goal_name.Ident.id_string,g))
th.S.theory_goals
in
let g = List.assoc g goals in
@@ -423,7 +424,7 @@ let element_latex_stat files n table dir e =
(fun fname file ->
let fname = Filename.basename fname in
let fname = List.hd (Str.split re_dot fname) in
- if fname = f then
+ if fname = f then
begin
found := true;
element_latex_stat_file file n table dir r