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

1 files changed, 17 insertions, 4 deletions

diff --git a/caml/RTLtypingaux.ml b/caml/RTLtypingaux.ml
index 64f839a..5ed7e6e 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, _, _) ->