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

5 files changed, 0 insertions, 24 deletions

diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index 9854117c..3506e502 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 b995132c..f369f9ea 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 d761f759..c4f45b22 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 2f2333fb..d2d2f24a 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 ff704ebe..632f2aa5 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) ->