Restrict (try...with...) to avoid catching critical exn (part 8)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 40 insertions, 36 deletions

diff --git a/lib/bigint.mli b/lib/bigint.mli
index 754f10d679..8b61a1fb61 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -11,6 +11,8 @@
 type bigint
 
 val of_string : string -> bigint
+(** May a Failure just as [int_of_string] on non-numerical strings *)
+
 val to_string : bigint -> string
 
 val of_int : int -> bigint
diff --git a/lib/errors.ml b/lib/errors.ml
index 27baf4314f..0d13fcd2f9 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -73,7 +73,7 @@ let rec print_gen bottom stk e =
     try h e
     with
     | Unhandled -> print_gen bottom stk' e
-    | e' -> print_gen bottom stk' e'
+    | any -> print_gen bottom stk' any
 
 (** Only anomalies should reach the bottom of the handler stack.
     In usual situation, the [handle_stack] is treated as it if was always
diff --git a/lib/flags.ml b/lib/flags.ml
index 4ad929052d..bd31b40248 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -9,18 +9,18 @@
 let with_option o f x =
   let old = !o in o:=true;
   try let r = f x in o := old; r
-  with e ->
-    let e = Backtrace.add_backtrace e in
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
     let () = o := old in
-    raise e
+    raise reraise
 
 let without_option o f x =
   let old = !o in o:=false;
   try let r = f x in o := old; r
-  with e ->
-    let e = Backtrace.add_backtrace e in
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
     let () = o := old in
-    raise e
+    raise reraise
 
 let boot = ref false
 
diff --git a/lib/pp.ml b/lib/pp.ml
index 99bd93411b..85c623f0c8 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -262,10 +262,10 @@ let pp_dirs ft =
   fun (dirstream : _ ppdirs) ->
     try
       Stream.iter pp_dir dirstream; com_brk ft
-    with e ->
-      let e = Backtrace.add_backtrace e in
+    with reraise ->
+      let reraise = Backtrace.add_backtrace reraise in
       let () = Format.pp_print_flush ft () in
-      raise e
+      raise reraise
 
 
 (* pretty print on stdout and stderr *)
diff --git a/lib/profile.ml b/lib/profile.ml
index b49a66e2f7..6f878d2f66 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -260,7 +260,7 @@ let time_overhead_B_C () =
       let _dw = dummy_spent_alloc () in
       let _dt = get_time () in
       ()
-    with _ -> assert false
+    with e when Errors.noncritical e -> assert false
   done;
   let after = get_time () in
   let beforeloop =  get_time () in
@@ -390,7 +390,7 @@ let profile1 e f a =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -403,7 +403,7 @@ let profile1 e f a =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile2 e f a b =
   let dw = spent_alloc () in
@@ -432,7 +432,7 @@ let profile2 e f a b =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -445,7 +445,7 @@ let profile2 e f a b =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile3 e f a b c =
   let dw = spent_alloc () in
@@ -474,7 +474,7 @@ let profile3 e f a b c =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -487,7 +487,7 @@ let profile3 e f a b c =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile4 e f a b c d =
   let dw = spent_alloc () in
@@ -516,7 +516,7 @@ let profile4 e f a b c d =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -529,7 +529,7 @@ let profile4 e f a b c d =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile5 e f a b c d g =
   let dw = spent_alloc () in
@@ -558,7 +558,7 @@ let profile5 e f a b c d g =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -571,7 +571,7 @@ let profile5 e f a b c d g =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile6 e f a b c d g h =
   let dw = spent_alloc () in
@@ -600,7 +600,7 @@ let profile6 e f a b c d g h =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -613,7 +613,7 @@ let profile6 e f a b c d g h =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile7 e f a b c d g h i =
   let dw = spent_alloc () in
@@ -642,7 +642,7 @@ let profile7 e f a b c d g h i =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -655,7 +655,7 @@ let profile7 e f a b c d g h i =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let print_logical_stats a =
   let (c, s, d) = CObj.obj_stats a in
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 218372afc2..7c82d6b80d 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -100,8 +100,8 @@ let abstract_eval_call handler c =
             | Quit -> Obj.magic (handler.quit () : unit)
             | About -> Obj.magic (handler.about () : coq_info)
           in Good res
-  with e ->
-    let (l, str) = handler.handle_exn e in
+  with any ->
+    let (l, str) = handler.handle_exn any in
     Fail (l,str)
 
 (** * XML data marshalling *)
@@ -282,7 +282,7 @@ let to_value f = function
         let loc_s = int_of_string (List.assoc "loc_s" attrs) in
         let loc_e = int_of_string (List.assoc "loc_e" attrs) in
         Some (loc_s, loc_e)
-      with _ -> None
+      with Not_found | Failure _ -> None
     in
     let msg = raw_string l in
     Fail (loc, msg)
diff --git a/lib/system.ml b/lib/system.ml
index 41201bd2d3..a72958b99b 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -105,12 +105,14 @@ let is_in_system_path filename =
   is_in_path lpath filename
 
 let open_trapping_failure name =
-  try open_out_bin name with _ -> error ("Can't open " ^ name)
+  try open_out_bin name
+  with e when Errors.noncritical e -> error ("Can't open " ^ name)
 
 let try_remove filename =
   try Sys.remove filename
-  with _ -> msg_warning
-    (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
+  with e when Errors.noncritical e ->
+    msg_warning
+      (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
 let marshal_out ch v = Marshal.to_channel ch v []
 let marshal_in filename ch =
@@ -143,10 +145,10 @@ let extern_intern ?(warn=true) magic suffix =
       try
         marshal_out channel val_0;
         close_out channel
-      with e ->
-	let e = Errors.push e in
+      with reraise ->
+	let reraise = Errors.push reraise in
         let () = try_remove filename in
-        raise e
+        raise reraise
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name =
     try
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
index 108e226783..630992eb5f 100644
--- a/lib/xml_parser.ml
+++ b/lib/xml_parser.ml
@@ -177,9 +177,9 @@ let do_parse xparser =
 		if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
 		Xml_lexer.close ();
 		x
-	with e ->
+	with any ->
 	  Xml_lexer.close ();
-	  raise (!xml_error (error_of_exn xparser e) xparser.source)
+	  raise (!xml_error (error_of_exn xparser any) xparser.source)
 
 let parse p = do_parse p