From 96383f6dbccd4b280acad395b9a2683a645a9de3 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 8 Jul 2019 10:48:24 +0200 Subject: Compatibility with OCaml 4.08 (#302) * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300 --- backend/Linearizeaux.ml | 2 +- backend/PrintAsm.ml | 3 +-- backend/PrintCminor.ml | 2 +- backend/PrintLTL.ml | 2 +- backend/PrintRTL.ml | 2 +- backend/PrintXTL.ml | 2 +- cparser/Cutil.ml | 2 +- debug/DwarfPrinter.ml | 4 ++-- driver/Interp.ml | 4 ++-- 9 files changed, 11 insertions(+), 12 deletions(-) diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 46d5c3f1..902724e0 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -106,7 +106,7 @@ let flatten_blocks blks = let cmp_minpc (mpc1, _) (mpc2, _) = if mpc1 = mpc2 then 0 else if mpc1 > mpc2 then -1 else 1 in - List.flatten (List.map Pervasives.snd (List.sort cmp_minpc blks)) + List.flatten (List.map snd (List.sort cmp_minpc blks)) (* Build the enumeration *) diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index dd428808..155f5e55 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -13,7 +13,6 @@ open AST open Camlcoq -open DwarfPrinter open PrintAsmaux open Printf open Sections @@ -177,7 +176,7 @@ module Printer(Target:TARGET) = let address = Target.address end - module DebugPrinter = DwarfPrinter (DwarfTarget) + module DebugPrinter = DwarfPrinter.DwarfPrinter (DwarfTarget) end let print_program oc p = diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index f68c1267..8c255a65 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -16,7 +16,7 @@ (** Pretty-printer for Cminor *) open Format -open Camlcoq +open !Camlcoq open Integers open AST open PrintAST diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index d0557073..1c449e74 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -112,7 +112,7 @@ let print_function pp id f = fprintf pp "%s() {\n" (extern_atom id); let instrs = List.sort - (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) (List.rev_map (fun (pc, i) -> (P.to_int pc, i)) (PTree.elements f.fn_code)) in diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index ba336b0a..841540b6 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -93,7 +93,7 @@ let print_function pp id f = fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; let instrs = List.sort - (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) (List.rev_map (fun (pc, i) -> (P.to_int pc, i)) (PTree.elements f.fn_code)) in diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml index cc1f7d49..6432682a 100644 --- a/backend/PrintXTL.ml +++ b/backend/PrintXTL.ml @@ -138,7 +138,7 @@ let print_function pp ?alloc ?live f = fprintf pp "f() {\n"; let instrs = List.sort - (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) (List.map (fun (pc, i) -> (P.to_int pc, i)) (PTree.elements f.fn_code)) in diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 5ff58780..7a2f4828 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -29,7 +29,7 @@ let no_loc = ("", -1) module Ident = struct type t = ident - let compare id1 id2 = Pervasives.compare id1.stamp id2.stamp + let compare id1 id2 = compare id1.stamp id2.stamp end module IdentSet = Set.Make(Ident) diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index bbfcf311..9a24041b 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -268,7 +268,7 @@ module DwarfPrinter(Target: DWARF_TARGET): (* Print the debug_abbrev section using the previous computed abbreviations*) let print_abbrev oc = let abbrevs = Hashtbl.fold (fun s i acc -> (s,i)::acc) abbrev_mapping [] in - let abbrevs = List.sort (fun (_,a) (_,b) -> Pervasives.compare a b) abbrevs in + let abbrevs = List.sort (fun (_,a) (_,b) -> compare a b) abbrevs in section oc Section_debug_abbrev; print_label oc !abbrev_start_addr; List.iter (fun (s,id) -> @@ -685,7 +685,7 @@ module DwarfPrinter(Target: DWARF_TARGET): print_label oc line_start; list_opt s (fun () -> section oc Section_debug_str; - let s = List.sort (fun (a,_) (b,_) -> Pervasives.compare a b) s in + let s = List.sort (fun (a,_) (b,_) -> compare a b) s in List.iter (fun (id,s) -> print_label oc (loc_to_label id); fprintf oc " .asciz %S\n" s) s) diff --git a/driver/Interp.ml b/driver/Interp.ml index 6760e76c..a6841460 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -15,7 +15,7 @@ open Format open Camlcoq open AST -open Integers +open !Integers open Values open Memory open Globalenvs @@ -145,7 +145,7 @@ let print_state p (prog, ge, s) = let compare_mem m1 m2 = (* assumes nextblocks were already compared equal *) (* should permissions be taken into account? *) - Pervasives.compare m1.Mem.mem_contents m2.Mem.mem_contents + compare m1.Mem.mem_contents m2.Mem.mem_contents (* Comparing continuations *) -- cgit