From e22118f5fe37a5129bf874fd7f49007d8b35b0f0 Mon Sep 17 00:00:00 2001
From: varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 12 Jul 2012 12:06:20 +0000
Subject: checklink: minor fixes

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1971 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 checklink/Check.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'checklink/Check.ml')

diff --git a/checklink/Check.ml b/checklink/Check.ml
index 8df09c5..c9fb67f 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -796,7 +796,7 @@ let check_sda ident ofs r addr ffw: f_framework or_err =
     let expected_addr = Safe32.(sym.st_value + ofs - addr) in
     try
       let r_addr = from_inferrable (IntMap.find r ffw.sf.ef.sda_map) in
-      if Safe32.(r_addr = expected_addr)
+      if r_addr = expected_addr
       then OK(ffw)
       else ERR(
         Printf.sprintf
@@ -3197,9 +3197,10 @@ let warn_sda_mapping efw =
         | Provided(vaddr, conflicts) ->
           efw
           >>> add_log (ERROR(
-            Printf.sprintf "Conflicting SDA mappings for register r%u:
-Specified: 0x%lX
-Expected: %s"
+            Printf.sprintf "
+    Conflicting SDA mappings for register r%u:
+      Specified: 0x%lX
+      Expected: %s"
               r vaddr (string_of_list (Printf.sprintf "0x%lX") ", " conflicts)
           ))
         | Inferred(vaddr, []) ->
@@ -3211,8 +3212,9 @@ Expected: %s"
         | Inferred(vaddr, conflicts) ->
           efw
           >>> add_log (ERROR(
-            Printf.sprintf "Conflicting SDA mappings for register r%u:
-%s"
+            Printf.sprintf "
+    Conflicting SDA mappings for register r%u:
+      %s"
               r (string_of_list (Printf.sprintf "0x%lX") ", " (vaddr :: conflicts))
           ))
       )
-- 
cgit v1.2.3