diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 12:07:11 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 12:07:11 +0000 |
commit | f6ecbb948ccf7f8a4e156eb29e3a41e7f2953407 (patch) | |
tree | ad958b2313ad00c2fdde49bd5f243f82d1e3ea58 /backend | |
parent | bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc (diff) | |
download | compcert-f6ecbb948ccf7f8a4e156eb29e3a41e7f2953407.tar.gz compcert-f6ecbb948ccf7f8a4e156eb29e3a41e7f2953407.zip |
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
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CMlexer.mll | 1 | ||||
-rw-r--r-- | backend/CMparser.mly | 11 | ||||
-rw-r--r-- | backend/CMtypecheck.ml | 9 | ||||
-rw-r--r-- | backend/Linearizeaux.ml | 1 | ||||
-rw-r--r-- | backend/RTLtypingaux.ml | 2 |
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) -> |