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

1 files changed, 4 insertions, 8 deletions

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 4407c67986..659ee4ec4b 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