From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 4 Aug 2007 07:27:50 +0000
Subject: Fusion des modifications faites sur les branches "tailcalls" et
 "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC
 - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout
 des langages intermediaires CminorSel et LTLin correspondants - Ajout des
 tailcalls depuis Cminor jusqu'a PPC

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

(limited to 'caml/RTLtypingaux.ml')

diff --git a/caml/RTLtypingaux.ml b/caml/RTLtypingaux.ml
index 64f839a2..5ed7e6e2 100644
--- a/caml/RTLtypingaux.ml
+++ b/caml/RTLtypingaux.ml
@@ -32,10 +32,6 @@ let type_instr retty (Coq_pair(pc, i)) =
       ()
   | Iop(Omove, _, _, _) -> 
       ()
-  | Iop(Oundef, Coq_nil, res, _) ->
-      ()
-  | Iop(Oundef, _, _, _) ->
-      raise (Type_error "wrong Oundef")
   | Iop(op, args, res, _) ->
       let (Coq_pair(targs, tres)) = type_of_operation op in
       set_types args targs; set_type res tres
@@ -61,6 +57,23 @@ let type_instr retty (Coq_pair(pc, i)) =
         raise(Type_error (Printf.sprintf "type mismatch in Icall(%s): %s"
                                          name msg))
       end
+  | Itailcall(sg, ros, args) ->
+      begin try
+        begin match ros with
+        | Coq_inl r -> set_type r Tint
+        | Coq_inr _ -> ()
+        end;
+        set_types args sg.sig_args;
+        if sg.sig_res <> retty then
+          raise (Type_error "mismatch on return type")
+      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 Itailcall(%s): %s"
+                                         name msg))
+      end
   | Ialloc(arg, res, _) ->
       set_type arg Tint; set_type res Tint
   | Icond(cond, args, _, _) ->
-- 
cgit