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/RTLtypingaux.ml | |
| 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/RTLtypingaux.ml')
| -rw-r--r-- | backend/RTLtypingaux.ml | 2 |
1 files changed, 0 insertions, 2 deletions
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) -> |