From 611e7b09253dbbb98e9cd4ca4e07a60b50e693fd Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 8 Jul 2008 12:04:42 +0000 Subject: Fusion partielle de la branche contsem: - semantiques a continuation pour Cminor et CminorSel - goto dans Cminor Suppression de backend/RTLbigstep.v, devenu inutile. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Selection.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v index a55b1918..6554e429 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -1153,6 +1153,8 @@ Fixpoint sel_stmt (s: Cminor.stmt) : stmt := | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs) | Cminor.Scall optid sg fn args => Scall optid sg (sel_expr fn) (sel_exprlist args) + | Cminor.Stailcall sg fn args => + Stailcall sg (sel_expr fn) (sel_exprlist args) | Cminor.Salloc id b => Salloc id (sel_expr b) | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2) | Cminor.Sifthenelse e ifso ifnot => @@ -1164,8 +1166,8 @@ Fixpoint sel_stmt (s: Cminor.stmt) : stmt := | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl | Cminor.Sreturn None => Sreturn None | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e)) - | Cminor.Stailcall sg fn args => - Stailcall sg (sel_expr fn) (sel_exprlist args) + | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body) + | Cminor.Sgoto lbl => Sgoto lbl end. (** Conversion of functions and programs. *) -- cgit