From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: Merge of the newmem branch: - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgen.v | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'backend/RTLgen.v') diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 28d2b069..86c11772 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -557,19 +557,28 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do no <- add_instr (Istore chunk addr rl r nd); do ns <- transl_expr map b r no; transl_exprlist map al rl ns - | Scall optid sig b cl => + | Scall optid sig (inl b) cl => do rf <- alloc_reg map b; do rargs <- alloc_regs map cl; do r <- alloc_optreg map optid; do n1 <- add_instr (Icall sig (inl _ rf) rargs r nd); do n2 <- transl_exprlist map cl rargs n1; transl_expr map b rf n2 - | Stailcall sig b cl => + | Scall optid sig (inr id) cl => + do rargs <- alloc_regs map cl; + do r <- alloc_optreg map optid; + do n1 <- add_instr (Icall sig (inr _ id) rargs r nd); + transl_exprlist map cl rargs n1 + | Stailcall sig (inl b) cl => do rf <- alloc_reg map b; do rargs <- alloc_regs map cl; do n1 <- add_instr (Itailcall sig (inl _ rf) rargs); do n2 <- transl_exprlist map cl rargs n1; transl_expr map b rf n2 + | Stailcall sig (inr id) cl => + do rargs <- alloc_regs map cl; + do n1 <- add_instr (Itailcall sig (inr _ id) rargs); + transl_exprlist map cl rargs n1 | Sbuiltin optid ef al => do rargs <- alloc_regs map al; do r <- alloc_optreg map optid; -- cgit