diff options
| author | Pierre-Marie Pédrot | 2013-11-24 00:59:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-11-24 00:59:41 +0100 |
| commit | dde0aa13213b1baad367c5d5f419010956ad2347 (patch) | |
| tree | 7793e031df5057659d8c4df99e7449d1c20c394e /lib | |
| parent | ae61e1397d343ee9b1e9a9715200e96706715e27 (diff) | |
Hardening the reading function of vo files.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/system.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/lib/system.ml b/lib/system.ml index 28af1ee40f..015124e5bc 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -134,10 +134,13 @@ let raw_extern_intern magic = output_binary_int channel magic; filename, channel and intern_state filename = - let channel = open_in_bin filename in - if not (Int.equal (input_binary_int channel) magic) then - raise (Bad_magic_number filename); - channel + try + let channel = open_in_bin filename in + if not (Int.equal (input_binary_int channel) magic) then + raise (Bad_magic_number filename); + channel + with End_of_file | Failure _ | Sys_error _ -> + error_corrupted filename in (extern_state,intern_state) |
