diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-02 08:03:05 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-02 08:03:05 +0200 |
commit | 97adfc372fd716c6701677b69950cd9279f46f27 (patch) | |
tree | 0f0b23f778074065d8920a9c55db81d36d854833 /lib/system.ml | |
parent | 54277abbf0fa15e0437d2a68859ceeef09ec70c3 (diff) | |
parent | bd5da52c6c625cb4559dd92051384383473ecb1b (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'lib/system.ml')
-rw-r--r-- | lib/system.ml | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/lib/system.ml b/lib/system.ml index 10ef8580b..e54109a2f 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -264,7 +264,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 @@ -274,8 +275,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" @@ -305,9 +310,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. *) |