diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-04 19:14:14 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-04 19:14:14 +0000 |
commit | 25b9b003178002360d666919f2e49e7f5f4a36e2 (patch) | |
tree | d5f7fb317f34f3a7ac9383c21b0eb143317c30f8 /cparser/SimplVolatile.ml | |
parent | 145b32ec504541e98f73b2c87ff2d8181b5e7968 (diff) | |
download | compcert-25b9b003178002360d666919f2e49e7f5f4a36e2.tar.gz compcert-25b9b003178002360d666919f2e49e7f5f4a36e2.zip |
Merge of the "volatile" branch:
- native treatment of volatile accesses in CompCert C's semantics
- translation of volatile accesses to built-ins in SimplExpr
- native treatment of struct assignment and passing struct parameter by value
- only passing struct result by value remains emulated
- in cparser, remove emulations that are no longer used
- added C99's type _Bool and used it to express || and && more efficiently.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cparser/SimplVolatile.ml')
-rw-r--r-- | cparser/SimplVolatile.ml | 81 |
1 files changed, 0 insertions, 81 deletions
diff --git a/cparser/SimplVolatile.ml b/cparser/SimplVolatile.ml deleted file mode 100644 index ef7a3a06..00000000 --- a/cparser/SimplVolatile.ml +++ /dev/null @@ -1,81 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Elimination of read-modify-write operators (+=, ++, etc) applied - to volatile expressions. *) - -open Printf -open C -open Cutil -open Transform - -(* Rewriting of expressions *) - -let transf_expr loc env ctx e = - - let is_volatile ty = - List.mem AVolatile (attributes_of_type env ty) in - - let rec texp ctx e = - match e.edesc with - | EConst _ -> e - | ESizeof _ -> e - | EVar _ -> e - | EUnop((Opreincr|Opredecr as op), e1) when is_volatile e1.etyp -> - expand_preincrdecr ~read:(fun e -> e) ~write:eassign - env ctx op (texp Val e1) - | EUnop((Opostincr|Opostdecr as op), e1) when is_volatile e1.etyp -> - expand_postincrdecr ~read:(fun e -> e) ~write:eassign - env ctx op (texp Val e1) - | EUnop(op, e1) -> - {edesc = EUnop(op, texp Val e1); etyp = e.etyp} - | EBinop(Oassign, e1, e2, ty) when is_volatile e1.etyp -> - expand_assign ~write:eassign env ctx (texp Val e1) (texp Val e2) - | EBinop((Oadd_assign | Osub_assign | Omul_assign - | Odiv_assign | Omod_assign - | Oand_assign | Oor_assign | Oxor_assign - | Oshl_assign | Oshr_assign) as op, e1, e2, ty) - when is_volatile e1.etyp -> - expand_assignop ~read:(fun e -> e) ~write:eassign - env ctx op (texp Val e1) (texp Val e2) ty - | EBinop(Ocomma, e1, e2, ty) -> - {edesc = EBinop(Ocomma, texp Effects e1, texp ctx e2, ty); - etyp = e.etyp} - | EBinop(op, e1, e2, ty) -> - {edesc = EBinop(op, texp Val e1, texp Val e2, ty); etyp = e.etyp} - | EConditional(e1, e2, e3) -> - {edesc = EConditional(texp Val e1, texp ctx e2, texp ctx e3); - etyp = e.etyp} - | ECast(ty, e1) -> - {edesc = ECast(ty, texp Val e1); etyp = e.etyp} - | ECall(e1, el) -> - {edesc = ECall(texp Val e1, List.map (texp Val) el); etyp = e.etyp} - - in texp ctx e - -(* Statements *) - -let transf_stmt env s = - Transform.stmt transf_expr env s - -(* Functions *) - -let transf_fundef env f = - Transform.fundef transf_stmt env f - -(* Programs *) - -let program p = - Transform.program ~fundef:transf_fundef p |