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

1 files changed, 11 insertions, 2 deletions

diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 28d2b06..86c1177 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;