aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/system.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-02 08:03:05 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-02 08:03:05 +0200
commit97adfc372fd716c6701677b69950cd9279f46f27 (patch)
tree0f0b23f778074065d8920a9c55db81d36d854833 /lib/system.ml
parent54277abbf0fa15e0437d2a68859ceeef09ec70c3 (diff)
parentbd5da52c6c625cb4559dd92051384383473ecb1b (diff)
Merge branch 'v8.5'
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml17
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. *)