Commit 9406e8a0 authored by MARCHE Claude's avatar MARCHE Claude

Merge remote-tracking branch 'adacore/lri-warnings'

Use module Warning whenever adequate
parents ce83f94d bc1c0b26
...@@ -415,7 +415,7 @@ let detect_unknown env detected = ...@@ -415,7 +415,7 @@ let detect_unknown env detected =
| None -> acc | None -> acc
| Some (priority,prover_id,prover_config) -> | Some (priority,prover_id,prover_config) ->
let prover = prover_config.prover in let prover = prover_config.prover in
eprintf "Warning: prover %s version %s is not known to be \ Warning.emit "Warning: prover %s version %s is not known to be \
supported.@." supported.@."
prover.Wc.prover_name prover.prover_version; prover.Wc.prover_name prover.prover_version;
(** Pb: Even if it match the first prover section (normally (** Pb: Even if it match the first prover section (normally
......
...@@ -399,7 +399,7 @@ let load_prover dirname (provers,shortcuts) section = ...@@ -399,7 +399,7 @@ let load_prover dirname (provers,shortcuts) section =
let shortcuts = add_prover_shortcuts shortcuts prover lshort in let shortcuts = add_prover_shortcuts shortcuts prover lshort in
provers,shortcuts provers,shortcuts
with MissingField s -> with MissingField s ->
eprintf "[Warning] cannot load a prover: missing field '%s'@." s; Warning.emit "[Warning] cannot load a prover: missing field '%s'@." s;
provers,shortcuts provers,shortcuts
...@@ -414,7 +414,7 @@ let load_shortcut acc section = ...@@ -414,7 +414,7 @@ let load_shortcut acc section =
prover_altern= altern} in prover_altern= altern} in
add_prover_shortcuts acc prover shortcuts add_prover_shortcuts acc prover shortcuts
with MissingField s -> with MissingField s ->
eprintf "[Warning] cannot load shortcut: missing field '%s'@." s; Warning.emit "[Warning] cannot load shortcut: missing field '%s'@." s;
acc acc
let load_editor editors (id, section) = let load_editor editors (id, section) =
...@@ -425,7 +425,7 @@ let load_editor editors (id, section) = ...@@ -425,7 +425,7 @@ let load_editor editors (id, section) =
editor_options = []; editor_options = [];
} editors } editors
with MissingField s -> with MissingField s ->
eprintf "[Warning] cannot load an editor: missing field '%s'@." s; Warning.emit "[Warning] cannot load an editor: missing field '%s'@." s;
editors editors
let load_policy provers acc (_,section) = let load_policy provers acc (_,section) =
...@@ -459,7 +459,7 @@ let load_policy provers acc (_,section) = ...@@ -459,7 +459,7 @@ let load_policy provers acc (_,section) =
| _ -> raise Not_found | _ -> raise Not_found
with Not_found -> acc with Not_found -> acc
with MissingField s -> with MissingField s ->
eprintf "[Warning] cannot load a policy: missing field '%s'@." s; Warning.emit "[Warning] cannot load a policy: missing field '%s'@." s;
acc acc
let load_strategy strategies section = let load_strategy strategies section =
...@@ -479,7 +479,7 @@ let load_strategy strategies section = ...@@ -479,7 +479,7 @@ let load_strategy strategies section =
strategies strategies
with with
MissingField s -> MissingField s ->
eprintf "[Warning] cannot load a strategy: missing field '%s'@." s; Warning.emit "[Warning] cannot load a strategy: missing field '%s'@." s;
strategies strategies
let load_main dirname section = let load_main dirname section =
...@@ -663,7 +663,7 @@ let merge_config config filename = ...@@ -663,7 +663,7 @@ let merge_config config filename =
let altern = get_stringo section "alternative" in let altern = get_stringo section "alternative" in
mk_filter_prover ?version ?altern name mk_filter_prover ?version ?altern name
with MissingField s -> with MissingField s ->
eprintf "[Warning] sec prover_modifiers is missing a '%s' field@." s; Warning.emit "[Warning] sec prover_modifiers is missing a '%s' field@." s;
mk_filter_prover "none" mk_filter_prover "none"
in in
let prover_modifiers = get_simple_family rc "prover_modifiers" in let prover_modifiers = get_simple_family rc "prover_modifiers" in
......
...@@ -1173,7 +1173,7 @@ let load_result r = ...@@ -1173,7 +1173,7 @@ let load_result r =
| "failure" -> Call_provers.Failure "" | "failure" -> Call_provers.Failure ""
| "highfailure" -> Call_provers.HighFailure | "highfailure" -> Call_provers.HighFailure
| s -> | s ->
eprintf Warning.emit
"[Warning] Session.load_result: unexpected status '%s'@." s; "[Warning] Session.load_result: unexpected status '%s'@." s;
Call_provers.HighFailure Call_provers.HighFailure
in in
...@@ -1190,7 +1190,8 @@ let load_result r = ...@@ -1190,7 +1190,8 @@ let load_result r =
| "undone" -> Interrupted | "undone" -> Interrupted
| "unedited" -> Unedited | "unedited" -> Unedited
| s -> | s ->
eprintf "[Warning] Session.load_result: unexpected element '%s'@." s; Warning.emit "[Warning] Session.load_result: unexpected element '%s'@."
s;
Interrupted Interrupted
let load_option attr g = let load_option attr g =
...@@ -1245,7 +1246,7 @@ let rec load_goal ctxt parent acc g = ...@@ -1245,7 +1246,7 @@ let rec load_goal ctxt parent acc g =
mg::acc mg::acc
| "label" -> acc | "label" -> acc
| s -> | s ->
eprintf "[Warning] Session.load_goal: unexpected element '%s'@." s; Warning.emit "[Warning] Session.load_goal: unexpected element '%s'@." s;
acc acc
and load_proof_or_transf ctxt mg a = and load_proof_or_transf ctxt mg a =
...@@ -1260,7 +1261,7 @@ and load_proof_or_transf ctxt mg a = ...@@ -1260,7 +1261,7 @@ and load_proof_or_transf ctxt mg a =
| [r] -> load_result r | [r] -> load_result r
| [] -> Interrupted | [] -> Interrupted
| _ -> | _ ->
eprintf "[Error] Too many result elements@."; Warning.emit "[Error] Too many result elements@.";
raise (LoadError (a,"too many result elements")) raise (LoadError (a,"too many result elements"))
in in
let edit = load_option "edited" a in let edit = load_option "edited" a in
...@@ -1283,7 +1284,7 @@ and load_proof_or_transf ctxt mg a = ...@@ -1283,7 +1284,7 @@ and load_proof_or_transf ctxt mg a =
in in
() ()
with Failure _ | Not_found -> with Failure _ | Not_found ->
eprintf "[Error] prover id not listed in header '%s'@." prover; Warning.emit "[Error] prover id not listed in header '%s'@." prover;
raise (LoadError (a,"prover not listing in header")) raise (LoadError (a,"prover not listing in header"))
end end
| "transf" -> | "transf" ->
...@@ -1302,7 +1303,7 @@ and load_proof_or_transf ctxt mg a = ...@@ -1302,7 +1303,7 @@ and load_proof_or_transf ctxt mg a =
| "metas" -> load_metas ctxt mg a; | "metas" -> load_metas ctxt mg a;
| "label" -> () | "label" -> ()
| s -> | s ->
eprintf Warning.emit
"[Warning] Session.load_proof_or_transf: unexpected element '%s'@." "[Warning] Session.load_proof_or_transf: unexpected element '%s'@."
s s
...@@ -1438,7 +1439,8 @@ let load_theory ctxt mf acc th = ...@@ -1438,7 +1439,8 @@ let load_theory ctxt mf acc th =
mth.theory_verified <- theory_verified mth; mth.theory_verified <- theory_verified mth;
mth::acc mth::acc
| s -> | s ->
eprintf "[Warning] Session.load_theory: unexpected element '%s'@." s; Warning.emit "[Warning] Session.load_theory: unexpected element '%s'@."
s;
acc acc
let load_file ~keygen session old_provers f = let load_file ~keygen session old_provers f =
...@@ -1471,11 +1473,11 @@ let load_file ~keygen session old_provers f = ...@@ -1471,11 +1473,11 @@ let load_file ~keygen session old_provers f =
prover_altern = altern} in prover_altern = altern} in
Mint.add id (p,timelimit,memlimit) old_provers Mint.add id (p,timelimit,memlimit) old_provers
with Failure _ -> with Failure _ ->
eprintf "[Warning] Session.load_file: unexpected non-numeric prover id '%s'@." id; Warning.emit "[Warning] Session.load_file: unexpected non-numeric prover id '%s'@." id;
old_provers old_provers
end end
| s -> | s ->
eprintf "[Warning] Session.load_file: unexpected element '%s'@." s; Warning.emit "[Warning] Session.load_file: unexpected element '%s'@." s;
old_provers old_provers
let load_session ~keygen session xml = let load_session ~keygen session xml =
...@@ -1494,7 +1496,8 @@ let load_session ~keygen session xml = ...@@ -1494,7 +1496,8 @@ let load_session ~keygen session xml =
old_provers; old_provers;
Debug.dprintf debug "[Info] load_session: done@\n" Debug.dprintf debug "[Info] load_session: done@\n"
| s -> | s ->
eprintf "[Warning] Session.load_session: unexpected element '%s'@." s Warning.emit "[Warning] Session.load_session: unexpected element '%s'@."
s
exception ShapesFileError of string exception ShapesFileError of string
exception SessionFileError of string exception SessionFileError of string
...@@ -1582,7 +1585,7 @@ let read_file_session_and_shapes dir xml_filename = ...@@ -1582,7 +1585,7 @@ let read_file_session_and_shapes dir xml_filename =
xml_filename compressed_shape_filename xml_filename compressed_shape_filename
else else
begin begin
Format.eprintf "[Warning] could not read goal shapes because \ Warning.emit "[Warning] could not read goal shapes because \
Why3 was not compiled with compress support@."; Why3 was not compiled with compress support@.";
Xml.from_file xml_filename, false Xml.from_file xml_filename, false
end end
...@@ -1592,11 +1595,11 @@ let read_file_session_and_shapes dir xml_filename = ...@@ -1592,11 +1595,11 @@ let read_file_session_and_shapes dir xml_filename =
ReadShapesNoCompress.read_xml_and_shapes xml_filename shape_filename ReadShapesNoCompress.read_xml_and_shapes xml_filename shape_filename
else else
begin begin
Format.eprintf "[Warning] could not find goal shapes file@."; Warning.emit "[Warning] could not find goal shapes file@.";
Xml.from_file xml_filename, false Xml.from_file xml_filename, false
end end
with e -> with e ->
Format.eprintf "[Warning] failed to read goal shapes: %s@." Warning.emit "[Warning] failed to read goal shapes: %s@."
(Printexc.to_string e); (Printexc.to_string e);
Xml.from_file xml_filename, false Xml.from_file xml_filename, false
...@@ -1621,7 +1624,7 @@ let read_session_with_keys ~keygen dir = ...@@ -1621,7 +1624,7 @@ let read_session_with_keys ~keygen dir =
(* xml does not exist yet *) (* xml does not exist yet *)
raise (SessionFileError msg) raise (SessionFileError msg)
| Xml.Parse_error s -> | Xml.Parse_error s ->
Format.eprintf "XML database corrupted, ignored (%s)@." s; Warning.emit "XML database corrupted, ignored (%s)@." s;
raise (SessionFileError "XML corrupted") raise (SessionFileError "XML corrupted")
else false else false
in in
......
...@@ -1178,7 +1178,7 @@ let rec eval_expr env (s:state) (e : expr) : result * state = ...@@ -1178,7 +1178,7 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
(Pp.print_option Pretty.print_loc) e.e_loc; (Pp.print_option Pretty.print_loc) e.e_loc;
Irred e, s Irred e, s
| _ -> | _ ->
eprintf "@[Warning: assertion cannot be evaluated at %a@]@." Warning.emit "@[Warning: assertion cannot be evaluated at %a@]@."
(Pp.print_option Pretty.print_loc) e.e_loc; (Pp.print_option Pretty.print_loc) e.e_loc;
Normal Vvoid, s Normal Vvoid, s
end end
......
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