From ca0e5f4fe9b4063991fa5e9eafe6a48f933b7c45 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 17 Sep 2006 08:58:31 +0000
Subject: Meilleur message de debug dans le cas Icall

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@102 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 caml/RTLtypingaux.ml | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'caml')

diff --git a/caml/RTLtypingaux.ml b/caml/RTLtypingaux.ml
index b76a0bb8..64f839a2 100644
--- a/caml/RTLtypingaux.ml
+++ b/caml/RTLtypingaux.ml
@@ -46,12 +46,21 @@ let type_instr retty (Coq_pair(pc, i)) =
       set_types args (type_of_addressing addr);
       set_type src (type_of_chunk chunk)
   | Icall(sg, ros, args, res, _) ->
-      begin match ros with
-      | Coq_inl r -> set_type r Tint
-      | Coq_inr _ -> ()
-      end;
-      set_types args sg.sig_args;
-      set_type res (match sg.sig_res with None -> Tint | Some ty -> ty)
+      begin try
+        begin match ros with
+        | Coq_inl r -> set_type r Tint
+        | Coq_inr _ -> ()
+        end;
+        set_types args sg.sig_args;
+        set_type res (match sg.sig_res with None -> Tint | Some ty -> ty)
+      with Type_error msg ->
+        let name =
+          match ros with
+          | Coq_inl _ -> "<reg>"
+          | Coq_inr id -> extern_atom id in
+        raise(Type_error (Printf.sprintf "type mismatch in Icall(%s): %s"
+                                         name msg))
+      end
   | Ialloc(arg, res, _) ->
       set_type arg Tint; set_type res Tint
   | Icond(cond, args, _, _) ->
-- 
cgit