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

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

5 files changed, 19 insertions, 17 deletions

diff --git a/library/nametab.mli b/library/nametab.mli
index d561735fd..43c174f1b 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -151,13 +151,15 @@ val path_of_tactic : ltac_constant -> full_path
 val dirpath_of_global : global_reference -> DirPath.t
 val basename_of_global : global_reference -> Id.t
 
-(** Printing of global references using names as short as possible *)
+(** Printing of global references using names as short as possible.
+    @raise Not_found when the reference is not in the global tables. *)
 val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds
 
 
 (** The [shortest_qualid] functions given an object with [user_name]
    Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and
-   Coq.A.B.x that denotes the same object. *)
+   Coq.A.B.x that denotes the same object.
+   @raise Not_found for unknown objects. *)
 
 val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid
 val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index ae60259e9..358fe2d01 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -402,8 +402,10 @@ let mono_filename f =
 	in
 	let id =
 	  if lang () <> Haskell then default_id
-	  else try Id.of_string (Filename.basename f)
-	  with _ -> error "Extraction: provided filename is not a valid identifier"
+	  else
+            try Id.of_string (Filename.basename f)
+	    with UserError _ ->
+              error "Extraction: provided filename is not a valid identifier"
 	in
 	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
 
@@ -541,7 +543,9 @@ let rec locate_ref = function
   | r::l ->
       let q = snd (qualid_of_reference r) in
       let mpo = try Some (Nametab.locate_module q) with Not_found -> None
-      and ro = try Some (Smartlocate.global_with_alias r) with _ -> None
+      and ro =
+        try Some (Smartlocate.global_with_alias r)
+        with Not_found | UserError _ -> None
       in
       match mpo, ro with
 	| None, None -> Nametab.error_global_not_found q
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 035f8e3bb..3ec9038c6 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -144,11 +144,11 @@ let sign_with_implicits r s nb_params =
 
 let rec handle_exn r n fn_name = function
   | MLexn s ->
-      (try Scanf.sscanf s "UNBOUND %d"
+      (try Scanf.sscanf s "UNBOUND %d%!"
 	 (fun i ->
 	    assert ((0 < i) && (i <= n));
 	    MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i)))
-       with _ -> MLexn s)
+       with Scanf.Scan_failure _ | End_of_file -> MLexn s)
   | a -> ast_map (handle_exn r n fn_name) a
 
 (*S Management of type variable contexts. *)
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 4407c6798..659ee4ec4 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -856,15 +856,11 @@ let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
     Unfolding them leads to more natural code (and more dummy removal) *)
 
 let is_program_branch = function
+  | Tmp _ | Dummy -> false
   | Id id ->
     let s = Id.to_string id in
-    let br = "program_branch_" in
-    let n = String.length br in
-    (try
-       ignore (int_of_string (String.sub s n (String.length s - n)));
-       String.sub s 0 n = br
-     with _ -> false)
-  | Tmp _ | Dummy -> false
+    try Scanf.sscanf s "program_branch_%d%!" (fun _ -> true)
+    with Scanf.Scan_failure _ | End_of_file -> false
 
 let expand_linear_let o id e =
    o.opt_lin_let || is_tmp id || is_program_branch id || is_imm_apply e
@@ -1297,7 +1293,7 @@ let inline_test r t =
     let c = match r with ConstRef c -> c | _ -> assert false in
     let has_body =
       try constant_has_body (Global.lookup_constant c)
-      with _ -> false
+      with Not_found -> false
     in
     has_body &&
       (let t1 = eta_red t in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 17303d80c..b35b5fc5e 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -255,7 +255,7 @@ let safe_basename_of_global r =
 
 let string_of_global r =
  try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r)
- with _ -> Id.to_string (safe_basename_of_global r)
+ with Not_found -> Id.to_string (safe_basename_of_global r)
 
 let safe_pr_global r = str (string_of_global r)
 
@@ -263,7 +263,7 @@ let safe_pr_global r = str (string_of_global r)
 
 let safe_pr_long_global r =
   try Printer.pr_global r
-  with _ -> match r with
+  with Not_found -> match r with
     | ConstRef kn ->
 	let mp,_,l = repr_con kn in
 	str ((string_of_mp mp)^"."^(Label.to_string l))