From 715388a4796aedb82cd6c7d5f51a21e3d655db4f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 26 May 2017 02:35:24 +0200 Subject: [votour] Fix build with -safe-string (bug 5553) --- checker/analyze.ml | 11 ++--------- checker/votour.ml | 3 +-- 2 files changed, 3 insertions(+), 11 deletions(-) diff --git a/checker/analyze.ml b/checker/analyze.ml index c48b83011..b406aa4c3 100644 --- a/checker/analyze.ml +++ b/checker/analyze.ml @@ -101,11 +101,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 +204,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 diff --git a/checker/votour.ml b/checker/votour.ml index 48f9f45e7..44ca8ef31 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -313,8 +313,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 -- cgit v1.2.3 From 26bc355c9a48db514efda6cb631f40b4f371ccef Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 26 May 2017 02:45:39 +0200 Subject: [votour] Fix/disable warnings. --- checker/analyze.ml | 4 +++- checker/votour.ml | 2 ++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/checker/analyze.ml b/checker/analyze.ml index b406aa4c3..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 @@ -244,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 44ca8ef31..9bfae7861 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -10,6 +10,7 @@ open Values (** {6 Interactive visit of a vo} *) +[@@@ocaml.warning "-52"] let rec read_num max = let quit () = Printf.printf "\nGoodbye!\n%!"; @@ -261,6 +262,7 @@ let pop () = match !stk with | i::s -> stk := s; i | _ -> failwith "empty stack" +[@@@ocaml.warning "-52"] let rec visit v o pos = Printf.printf "\nDepth %d Pos %s Context %s\n" (List.length !stk) -- cgit v1.2.3 From 6de0e0faf3b7f2419972ebfeb90f3fa21c5657fe Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 26 May 2017 17:48:43 +0200 Subject: [checker] Add bin/votour to the coqocaml target. --- Makefile.dev | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3 From 1b0d3a835929fc3d84e3d32c84f79adadb5c9157 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 26 May 2017 20:46:21 +0200 Subject: [checker] [votour] resolve warning 52 fragile constant pattern Also stop using failwith for flow control in tuple_of_string. --- checker/votour.ml | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/checker/votour.ml b/checker/votour.ml index 9bfae7861..c255e5cdb 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -10,7 +10,6 @@ open Values (** {6 Interactive visit of a vo} *) -[@@@ocaml.warning "-52"] let rec read_num max = let quit () = Printf.printf "\nGoodbye!\n%!"; @@ -20,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! enters the -th child, u goes up 1 level, x exits\n%!"; read_num max @@ -150,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 *) @@ -206,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 @@ -237,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 @@ -258,11 +259,11 @@ 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 -[@@@ocaml.warning "-52"] let rec visit v o pos = Printf.printf "\nDepth %d Pos %s Context %s\n" (List.length !stk) @@ -285,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 -- cgit v1.2.3