Merge PR#681: Fix votour for safe strings & warnings

3 files changed, 19 insertions, 22 deletions

diff --git a/Makefile.dev b/Makefile.dev
index 1803cc8ff..fde92ec94 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -98,7 +98,7 @@ pluginsopt: $(PLUGINSOPT)
 pluginsbyte: $(PLUGINS)
 
 # This should build all the ocaml code but not (most of) the .v files
-coqocaml: tools coqbinaries pluginsopt coqide printers
+coqocaml: tools coqbinaries pluginsopt coqide printers bin/votour
 
 .PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml
 
diff --git a/checker/analyze.ml b/checker/analyze.ml
index c48b83011..df75d5b93 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -4,6 +4,7 @@ let prefix_small_block =         0x80
 let prefix_small_int =           0x40
 let prefix_small_string =        0x20
 
+[@@@ocaml.warning "-32"]
 let code_int8 =                  0x00
 let code_int16 =                 0x01
 let code_int32 =                 0x02
@@ -25,6 +26,7 @@ let code_infixpointer =          0x11
 let code_custom =                0x12
 let code_block64 =               0x13
 
+[@@@ocaml.warning "-37"]
 type code_descr =
 | CODE_INT8
 | CODE_INT16
@@ -101,11 +103,11 @@ let input_binary_int chan =
   input_binary_int chan
 
 let input_char chan = Char.chr (input_byte chan)
+let input_string len chan = String.init len (fun _ -> input_char chan)
 
 let parse_header chan =
   let () = current_offset := 0 in
-  let magic = String.create 4 in
-  let () = for i = 0 to 3 do magic.[i] <- input_char chan done in
+  let magic = input_string 4 chan in
   let length = input_binary_int chan in
   let objects = input_binary_int chan in
   let size32 = input_binary_int chan in
@@ -204,13 +206,6 @@ let input_header64 chan =
   in
   (tag, len)
 
-let input_string len chan =
-  let ans = String.create len in
-  for i = 0 to pred len do
-    ans.[i] <- input_char chan;
-  done;
-  ans
-
 let parse_object chan =
   let data = input_byte chan in
   if prefix_small_block <= data then
@@ -251,7 +246,7 @@ let parse_object chan =
     RString (input_string len chan)
   | CODE_CODEPOINTER ->
     let addr = input_int32u chan in
-    for i = 0 to 15 do ignore (input_byte chan); done;
+    for _i = 0 to 15 do ignore (input_byte chan); done;
     RCode addr
   | CODE_DOUBLE_ARRAY32_LITTLE
   | CODE_DOUBLE_BIG
diff --git a/checker/votour.ml b/checker/votour.ml
index 48f9f45e7..c255e5cdb 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -19,14 +19,14 @@ let rec read_num max =
   if l = "u" then None
   else if l = "x" then quit ()
   else
-    try
-      let v = int_of_string l in
+    match int_of_string l with
+    | v ->
       if v < 0 || v >= max then
         let () =
           Printf.printf "Out-of-range input! (only %d children)\n%!" max in
         read_num max
       else Some v
-    with Failure "int_of_string" ->
+    | exception Failure _ ->
       Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!";
       read_num max
 
@@ -149,16 +149,17 @@ let rec get_name ?(extra=false) = function
 (** For tuples, its quite handy to display the inner 1st string (if any).
     Cf. [structure_body] for instance *)
 
+exception TupleString of string
 let get_string_in_tuple o =
   try
     for i = 0 to Array.length o - 1 do
       match Repr.repr o.(i) with
       | STRING s ->
-        failwith (Printf.sprintf " [..%s..]" s)
+        raise (TupleString (Printf.sprintf " [..%s..]" s))
       | _ -> ()
     done;
     ""
-  with Failure s -> s
+  with TupleString s -> s
 
 (** Some details : tags, integer value for non-block, etc etc *)
 
@@ -205,6 +206,7 @@ let access_block o = match Repr.repr o with
 let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit
 
 (** raises Exit if the object has not the expected structure *)
+exception Forbidden
 let rec get_children v o pos = match v with
   |Tuple (_, v) ->
     let (_, os) = access_block o in
@@ -236,7 +238,7 @@ let rec get_children v o pos = match v with
       [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|]
     | _ -> raise Exit
     end
-  |Fail s -> failwith "forbidden"
+  |Fail s -> raise Forbidden
 
 let get_children v o pos =
   try get_children v o pos
@@ -257,9 +259,10 @@ let init () = stk := []
 
 let push name v o p = stk := { nam = name; typ = v; obj = o; pos = p } :: !stk
 
+exception EmptyStack
 let pop () = match !stk with
   | i::s -> stk := s; i
-  | _ -> failwith "empty stack"
+  | _ -> raise EmptyStack
 
 let rec visit v o pos =
   Printf.printf "\nDepth %d Pos %s Context %s\n"
@@ -283,8 +286,8 @@ let rec visit v o pos =
        push (get_name v) v o pos;
        visit v' o' pos'
   with
-  | Failure "empty stack" -> ()
-  | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos
+  | EmptyStack -> ()
+  | Forbidden -> let info = pop () in visit info.typ info.obj info.pos
   | Failure _ | Invalid_argument _ -> visit v o pos
 
 end
@@ -313,8 +316,7 @@ let dummy_header = {
 }
 
 let parse_header chan =
-  let magic = String.create 4 in
-  let () = for i = 0 to 3 do magic.[i] <- input_char chan done in
+  let magic = really_input_string chan 4 in
   let length = input_binary_int chan in
   let objects = input_binary_int chan in
   let size32 = input_binary_int chan in