diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.mllib | 2 | ||||
| -rw-r--r-- | checker/checker.ml | 8 | ||||
| -rw-r--r-- | checker/safe_typing.ml | 6 | ||||
| -rw-r--r-- | checker/votour.ml | 11 |
4 files changed, 16 insertions, 11 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 0d36e3a0f1..3725989e87 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -8,6 +8,7 @@ Hashcons CSet CMap Int +Dyn HMap Option Store @@ -35,6 +36,7 @@ Errors Ephemeron Future CUnix + System Profile RemoteCounter diff --git a/checker/checker.ml b/checker/checker.ml index d5d9b9e3b8..da93685f98 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -217,12 +217,6 @@ open Type_errors let anomaly_string () = str "Anomaly: " let report () = (str "." ++ spc () ++ str "Please report.") -let print_loc loc = - if loc = Loc.ghost then - (str"<unknown>") - else - let loc = Loc.unloc loc in - (int (fst loc) ++ str"-" ++ int (snd loc)) let guill s = str "\"" ++ str s ++ str "\"" let where s = @@ -337,8 +331,6 @@ let parse_args argv = | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem - | "-R" :: d :: "-as" :: [] -> usage () | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem | "-R" :: ([] | [_]) -> usage () diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 81a3cc035b..ee33051676 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -13,6 +13,8 @@ open Cic open Names open Environ +let pr_dirpath dp = str (DirPath.to_string dp) + (************************************************************************) (* * Global environment @@ -52,9 +54,9 @@ let check_engagement env (expected_impredicative_set,expected_type_in_type) = let report_clash f caller dir = let msg = - str "compiled library " ++ str(DirPath.to_string caller) ++ + str "compiled library " ++ pr_dirpath caller ++ spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++ - str(DirPath.to_string dir) ++ fnl() in + pr_dirpath dir ++ fnl() in f msg diff --git a/checker/votour.ml b/checker/votour.ml index 4aecb28f20..f8264ca684 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -22,6 +22,7 @@ sig val input : in_channel -> obj val repr : obj -> obj repr val size : obj -> int + val oid : obj -> int option end module ReprObj : S = @@ -45,6 +46,7 @@ struct else INT (Obj.magic obj) let size (_, p) = CObj.shared_size_of_pos p + let oid _ = None end module ReprMem : S = @@ -97,6 +99,9 @@ struct let _ = init_size seen obj in obj + let oid = function + | Int _ | Atm _ | Fun _ -> None + | Ptr p -> Some p end module Visit (Repr : S) : @@ -149,9 +154,13 @@ let rec get_details v o = match v, Repr.repr o with |Annot (s,v), _ -> get_details v o |_ -> "" +let get_oid obj = match Repr.oid obj with +| None -> "" +| Some id -> Printf.sprintf " [0x%08x]" id + let node_info (v,o,p) = get_name ~extra:true v ^ get_details v o ^ - " (size "^ string_of_int (Repr.size o)^"w)" + " (size "^ string_of_int (Repr.size o)^"w)" ^ get_oid o (** Children of a block : type, object, position. For lists, we collect all elements of the list at once *) |