diff options
| author |  Tej Chajed <tchajed@mit.edu> | 2016-04-09 12:46:40 -0400 |
|---|---|---|
| committer |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-25 18:48:39 +0200 |
| commit | dc469f9aaf0d5b77458e40893d897de12339b9b3 (patch) | |
| tree | e6f77723aa86e4ec766eadda10bb001dbf55b30e /lib | |
| parent | b295d3402ddebfd2ca3aa052a32880df8d9060a2 (diff) | |
Print magic numbers in bad magic error message
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/system.ml | 17 | ||||
| -rw-r--r-- | lib/system.mli | 6 |
2 files changed, 16 insertions, 7 deletions
diff --git a/lib/system.ml b/lib/system.ml index 36fdf2608..205a5506c 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -214,7 +214,8 @@ let skip_in_segment f ch = seek_in ch stop; stop, digest_in f ch -exception Bad_magic_number of string +type magic_number_error = {filename: string; actual: int; expected: int} +exception Bad_magic_number of magic_number_error let raw_extern_state magic filename = let channel = open_trapping_failure filename in @@ -224,8 +225,12 @@ let raw_extern_state magic filename = let raw_intern_state magic filename = try let channel = open_in_bin filename in - if not (Int.equal (input_binary_int filename channel) magic) then - raise (Bad_magic_number filename); + let actual_magic = input_binary_int filename channel in + if not (Int.equal actual_magic magic) then + raise (Bad_magic_number { + filename=filename; + actual=actual_magic; + expected=magic}); channel with | End_of_file -> error_corrupted filename "premature end of file" @@ -255,9 +260,11 @@ let intern_state magic filename = let with_magic_number_check f a = try f a - with Bad_magic_number fname -> + with Bad_magic_number {filename=fname;actual=actual;expected=expected} -> errorlabstrm "with_magic_number_check" - (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++ + (str"File " ++ str fname ++ strbrk" has bad magic number " ++ + int actual ++ str" (expected " ++ int expected ++ str")." ++ + spc () ++ strbrk "It is corrupted or was compiled with another version of Coq.") (* Time stamps. *) diff --git a/lib/system.mli b/lib/system.mli index 062c8ea85..fa675a4f0 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -34,9 +34,11 @@ val file_exists_respecting_case : string -> string -> bool (** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] - when the check fails, with the full file name. *) + when the check fails, with the full file name and expected/observed magic + numbers. *) -exception Bad_magic_number of string +type magic_number_error = {filename: string; actual: int; expected: int} +exception Bad_magic_number of magic_number_error val raw_extern_state : int -> string -> out_channel |