summaryrefslogtreecommitdiff
path: root/checklink
diff options
context:
space:
mode:
Diffstat (limited to 'checklink')
-rw-r--r--checklink/Asm_printers.ml1
-rw-r--r--checklink/Check.ml8
-rw-r--r--checklink/Library.ml3
3 files changed, 12 insertions, 0 deletions
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml
index aeb4b3f..00b6e2e 100644
--- a/checklink/Asm_printers.ml
+++ b/checklink/Asm_printers.ml
@@ -221,6 +221,7 @@ let string_of_init_data = function
| Init_int8(i) -> "Init_int8(" ^ string_of_int (z_int_lax i) ^ ")"
| Init_int16(i) -> "Init_int16(" ^ string_of_int (z_int_lax i) ^ ")"
| Init_int32(i) -> "Init_int32(" ^ string_of_int32i (z_int32 i) ^ ")"
+| Init_int64(i) -> "Init_int64(" ^ string_of_int64i (z_int64 i) ^ ")"
| Init_float32(f) -> "Init_float32(" ^ string_of_ffloat f ^ ")"
| Init_float64(f) -> "Init_float64(" ^ string_of_ffloat f ^ ")"
| Init_space(z) -> "Init_space(" ^ string_of_int (z_int z) ^ ")"
diff --git a/checklink/Check.ml b/checklink/Check.ml
index 5821953..73a7310 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -2696,6 +2696,14 @@ let compare_data (l: init_data list) (bs: bitstring) (sfw: s_framework)
else ERR("Wrong float64")
| { _ } -> error
)
+ | Init_int64(i) -> (
+ bitmatch bs with
+ | { j : 64 : int; bs : -1 : bitstring } ->
+ if z_int64 i = j
+ then compare_data_aux l bs (s + 8) sfw
+ else ERR("Wrong int64")
+ | { _ } -> error
+ )
| Init_space(z) -> (
let space_size = z_int z in
bitmatch bs with
diff --git a/checklink/Library.ml b/checklink/Library.ml
index acea80a..69a0d6e 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -110,6 +110,8 @@ let z_int z = Safe32.to_int (z_int32 z)
let z_int_lax z = Safe32.to_int (z_int32_lax z)
+let z_int64 = Camlcoq.Z.to_int64
+
(* Some more printers *)
let string_of_ffloat f = string_of_float (camlfloat_of_coqfloat f)
@@ -144,6 +146,7 @@ let string_of_int32 = Printf.sprintf "0x%08lx"
let string_of_int64 = Printf.sprintf "0x%08Lx"
(* To print counts/indices *)
let string_of_int32i = Int32.to_string
+let string_of_int64i = Int64.to_string
let string_of_positive p = string_of_int32i (positive_int32 p)