From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jan 2013 09:10:29 +0000 Subject: Ported to Coq 8.4pl1. Merge of branches/coq-8.4. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Check.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'checklink/Check.ml') diff --git a/checklink/Check.ml b/checklink/Check.ml index a1cc004..9d668fa 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -1,8 +1,7 @@ +open Camlcoq open Asm open Asm_printers open AST -open BinInt -open BinPos open Bitstring_utils open C2C open Camlcoq @@ -204,7 +203,7 @@ let re_variadic_stub: Str.regexp = Str.regexp "\\(.*\\)\\$[if]*$" address, unless the symbol is a stub from CompCert. Otherwise, it filters out all symbols whose virtual address does not match [vaddr]. *) -let idmap_unify (k: positive) (vaddr: int32) (sfw: s_framework) +let idmap_unify (k: P.t) (vaddr: int32) (sfw: s_framework) : s_framework or_err = try ( (* get the list of possible symbols for ident [k] *) @@ -438,13 +437,13 @@ let match_csts (cc: constant) (ec: int32): checker = fun ffw -> (* sda should be handled separately in places it occurs *) fatal "Unhandled Csymbol_sda, please report." -let match_z_int32 (cz: coq_Z) (ei: int32) = +let match_z_int32 (cz: Z.t) (ei: int32) = let cz = z_int32 cz in check_eq ( Printf.sprintf "match_z_int32 %s %s" (string_of_int32 cz) (string_of_int32 ei) ) cz ei -let match_z_int (cz: coq_Z) (ei: int) = +let match_z_int (cz: Z.t) (ei: int) = let cz = z_int32 cz in let ei = Safe32.of_int ei in check_eq ( @@ -452,7 +451,7 @@ let match_z_int (cz: coq_Z) (ei: int) = ) cz ei (* [m] is interpreted as a bitmask, and checked against [ei]. *) -let match_mask (m: coq_Z) (ei: int32) = +let match_mask (m: Z.t) (ei: int32) = let m = z_int32_lax m in check_eq ( Printf.sprintf "match_mask %s %s" -- cgit v1.2.3