diff options
| author | Pierre-Marie Pédrot | 2020-03-13 14:07:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-13 14:07:01 +0100 |
| commit | 3449c8a088e9a902ebc73478667f4f25d6c08d2a (patch) | |
| tree | 48e1056448a2aad68ddfc56c7a8466126daadbc6 | |
| parent | b6e6751011bc3ede5da75394ef2ed9396b28f87f (diff) | |
| parent | dfa74b252c236ae6fe2f36e2f091ddad8ae7e259 (diff) | |
Merge PR #11805: Fix coqchk for primitive integers on 32bit arch with OCaml >= 4.08 (#11624)
Reviewed-by: ppedrot
| -rw-r--r-- | checker/analyze.ml | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/checker/analyze.ml b/checker/analyze.ml index 91137a0ce2..94acba6b05 100644 --- a/checker/analyze.ml +++ b/checker/analyze.ml @@ -25,6 +25,12 @@ let code_codepointer = 0x10 let code_infixpointer = 0x11 let code_custom = 0x12 let code_block64 = 0x13 +let code_shared64 = 0x14 +let code_string64 = 0x15 +let code_double_array64_big = 0x16 +let code_double_array64_little = 0x17 +let code_custom_len = 0x18 +let code_custom_fixed = 0x19 [@@@ocaml.warning "-37"] type code_descr = @@ -48,8 +54,14 @@ type code_descr = | CODE_INFIXPOINTER | CODE_CUSTOM | CODE_BLOCK64 +| CODE_SHARED64 +| CODE_STRING64 +| CODE_DOUBLE_ARRAY64_BIG +| CODE_DOUBLE_ARRAY64_LITTLE +| CODE_CUSTOM_LEN +| CODE_CUSTOM_FIXED -let code_max = 0x13 +let code_max = 0x19 let magic_number = "\132\149\166\190" @@ -342,7 +354,8 @@ let parse_object chan = let addr = input_int32u chan in for _i = 0 to 15 do ignore (input_byte chan); done; RCode addr - | CODE_CUSTOM -> + | CODE_CUSTOM + | CODE_CUSTOM_FIXED -> begin match input_cstring chan with | "_j" -> Rint64 (input_intL chan) | s -> Printf.eprintf "Unhandled custom code: %s" s; assert false @@ -356,6 +369,11 @@ let parse_object chan = | CODE_DOUBLE_ARRAY8_LITTLE | CODE_DOUBLE_ARRAY32_BIG | CODE_INFIXPOINTER + | CODE_SHARED64 + | CODE_STRING64 + | CODE_DOUBLE_ARRAY64_BIG + | CODE_DOUBLE_ARRAY64_LITTLE + | CODE_CUSTOM_LEN -> Printf.eprintf "Unhandled code %04x\n%!" data; assert false let parse chan = |