From 8aa2e600d375caffef47058f1d095777a0dfdbb0 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 12 Mar 2013 23:59:28 +0000 Subject: Restrict (try...with...) to avoid catching critical exn (part 1) Why? : avoid catching (and probably ignoring) exceptions such as Sys.Break, anomalies, assertions, leading to undetected bugs and ignored Ctrl-C. How? : when the precise exception(s) concerned by the try is known, use them explicitely in the "with". Otherwise, let's use the pattern "with e when Errors.noncritical e -> " Particular case : when an exception is catched and reraised immediately after some adjustments, we leave it untouched. Simply, for easily identifying these situations later, the name of the exception variable is changed to "reraise". Please also adopt this coding style. Automatic checks based on the "mascot" tool of X. Clerc will be runned regularly. If you want to avoid to check a particular try...with, use the variable name "any" after the "with". All these changes have been tested using the standard library and the test-suite, but unfortunately this is far from ensuring that coqtop behaves as before. We'll see after the nightly bench... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16276 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/checker.ml | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) (limited to 'checker/checker.ml') diff --git a/checker/checker.ml b/checker/checker.ml index 9834b1331..10a3089ed 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -70,8 +70,9 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Id.of_string d - with _ -> - if_verbose msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + with Errors.UserError _ -> + if_verbose msg_warning + (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); raise Exit let add_rec_path ~unix_path ~coq_root = @@ -279,9 +280,9 @@ let rec explain_exn = function report ()) | e when is_anomaly e -> print_anomaly e - | reraise -> + | e -> hov 0 (anomaly_string () ++ str "Uncaught exception " ++ - str (Printexc.to_string reraise)++report()) + str (Printexc.to_string e)++report()) let parse_args argv = let rec parse = function @@ -334,13 +335,7 @@ let parse_args argv = fatal_error (str "Unknown option " ++ str s) | s :: rem -> add_compile s; parse rem in - try - parse (List.tl (Array.to_list argv)) - with - | UserError(_, s) as e -> - if Pp.is_empty s then exit 1 - else fatal_error (explain_exn e) - | e -> begin fatal_error (explain_exn e) end + parse (List.tl (Array.to_list argv)) (* To prevent from doing the initialization twice *) -- cgit v1.2.3