Elimination of "alloc" instruction in Caml files and test files.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

8 files changed, 4 insertions, 30 deletions

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index e5b21f9..16f22d6 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -336,8 +336,6 @@ let print_instruction oc labels = function
   | Psufd(r1, r2, r3) ->
       fprintf oc "	sufd	%a, %a, %a\n" freg r1 freg r2 freg r3; 1
   (* Pseudo-instructions *)
-  | Pallocblock ->
-      fprintf oc "	bl	compcert_alloc\n"; 1
   | Pallocframe(lo, hi, ofs) ->
       let lo = camlint_of_coqint lo
       and hi = camlint_of_coqint hi
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index 9854117..3506e50 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -33,7 +33,6 @@ rule token = parse
   | blank +      { token lexbuf }
   | "/*"         { comment lexbuf; token lexbuf }
   | "absf" { ABSF }
-  | "alloc" { ALLOC }
   | "&" { AMPERSAND }
   | "&&" { AMPERSANDAMPERSAND }
   | "!"    { BANG }
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index b995132..f369f9e 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -33,7 +33,6 @@ type rexpr =
   | Rload of memory_chunk * rexpr
   | Rcondition of rexpr * rexpr * rexpr
   | Rcall of signature * rexpr * rexpr list
-  | Ralloc of rexpr
 
 let temp_counter = ref 0
 
@@ -68,11 +67,6 @@ let rec convert_rexpr = function
       let t = mktemp() in
       convert_accu := Scall(Some t, sg, c1, cl) :: !convert_accu;
       Evar t
-  | Ralloc e1 ->
-      let c1 = convert_rexpr e1 in
-      let t = mktemp() in
-      convert_accu := Salloc(t, c1) :: !convert_accu;
-      Evar t
 
 and convert_rexpr_list = function
   | [] -> []
@@ -104,9 +98,6 @@ let mkassign id e =
       let c1 = convert_rexpr e1 in
       let cl = convert_rexpr_list el in
       prepend_seq !convert_accu (Scall(Some id, sg, c1, cl))
-  | Ralloc(e1) ->
-      let c1 = convert_rexpr e1 in
-      prepend_seq !convert_accu (Salloc(id, c1))
   | _ ->
       let c = convert_rexpr e in
       prepend_seq !convert_accu (Sassign(id, c))
@@ -206,7 +197,6 @@ let mkmatch expr cases =
 %token ABSF
 %token AMPERSAND
 %token AMPERSANDAMPERSAND
-%token ALLOC
 %token BANG
 %token BANGEQUAL
 %token BANGEQUALF
@@ -508,7 +498,6 @@ expr:
   | expr BARBAR expr                            { orbool $1 $3 }
   | expr QUESTION expr COLON expr               { Rcondition($1, $3, $5) }
   | expr LPAREN expr_list RPAREN COLON signature{ Rcall($6, $1, $3) }
-  | ALLOC expr                                  { Ralloc $2 }
 ;
 
 expr_list:
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index d761f75..c4f45b2 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -294,15 +294,6 @@ let rec type_stmt env blk ret s =
       with Error s ->
         raise (Error (sprintf "In call:\n%s" s))
       end
-  | Salloc(id, e) ->
-      let tid = type_var env id in
-      let te = type_expr env [] e in
-      begin try
-        unify tint te;
-        unify tint tid
-      with Error s ->
-        raise (Error (sprintf "In alloc:\n%s" s))
-      end
   | Sseq(s1, s2) ->
       type_stmt env blk ret s1;
       type_stmt env blk ret s2
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 2f2333f..d2d2f24 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -70,7 +70,6 @@ let enumerate_aux f reach =
            | Lstore (chunk, addr, args, src, s) -> emit_block pending s
            | Lcall (sig0, ros, args, res, s) -> emit_block pending s
            | Ltailcall (sig0, ros, args) -> emit_restart pending
-           | Lalloc (arg, res, s) -> emit_block pending s
            | Lcond (cond, args, ifso, ifnot) ->
                emit_restart (IntSet.add (int_of_pos ifso)
                              (IntSet.add (int_of_pos ifnot) pending))
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
index ff704eb..632f2aa 100644
--- a/backend/RTLtypingaux.ml
+++ b/backend/RTLtypingaux.ml
@@ -86,8 +86,6 @@ let type_instr retty (Coq_pair(pc, i)) =
         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, _, _) ->
       set_types args (type_of_condition cond)
   | Ireturn(optres) ->
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index a52a90f..352da05 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -180,8 +180,6 @@ let print_instruction oc labels = function
       fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
   | Paddze(r1, r2) ->
       fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
-  | Pallocblock ->
-      fprintf oc "	bl	%a\n" raw_symbol "compcert_alloc"
   | Pallocframe(lo, hi, ofs) ->
       let lo = camlint_of_coqint lo
       and hi = camlint_of_coqint hi
diff --git a/test/cminor/lists.cm b/test/cminor/lists.cm
index c445623..6007f3c 100644
--- a/test/cminor/lists.cm
+++ b/test/cminor/lists.cm
@@ -1,11 +1,13 @@
 /* List manipulations */
 
+extern "malloc" : int -> int
+
 "buildlist"(n): int -> int
 {
   var b;
 
   if (n < 0) return 0;
-  b = alloc 8;
+  b = "malloc"(8) : int -> int;
   int32[b] = n;
   int32[b+4] = "buildlist"(n - 1) : int -> int;
   return b;
@@ -17,7 +19,7 @@
   r = 0;
   loop {
     if (l == 0) return r;
-    r2 = alloc 8;
+    r2 = "malloc"(8) : int -> int;
     int32[r2] = int32[l];
     int32[r2+4] = r;
     r = r2;