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

13 files changed, 31 insertions, 1243 deletions

diff --git a/cparser/.depend b/cparser/.depend
index 51f3b5e..4a7f538 100644
--- a/cparser/.depend
+++ b/cparser/.depend
@@ -1,4 +1,3 @@
-AddCasts.cmi: C.cmi
 Bitfields.cmi: C.cmi
 Builtins.cmi: Env.cmi C.cmi
 C.cmi:
@@ -12,18 +11,13 @@ Errors.cmi:
 GCC.cmi: Builtins.cmi
 Lexer.cmi: Parser.cmi
 Machine.cmi:
-PackedStructs.cmi: C.cmi
 Parse.cmi: C.cmi
 Parse_aux.cmi:
 Parser.cmi: Cabs.cmo
 Rename.cmi: C.cmi
-SimplExpr.cmi: C.cmi
-StructAssign.cmi: C.cmi
-StructByValue.cmi: C.cmi
+StructReturn.cmi: C.cmi
 Transform.cmi: Env.cmi C.cmi
 Unblock.cmi: C.cmi
-AddCasts.cmo: Transform.cmi Cutil.cmi C.cmi AddCasts.cmi
-AddCasts.cmx: Transform.cmx Cutil.cmx C.cmi AddCasts.cmi
 Bitfields.cmo: Transform.cmi Machine.cmi Cutil.cmi C.cmi Bitfields.cmi
 Bitfields.cmx: Transform.cmx Machine.cmx Cutil.cmx C.cmi Bitfields.cmi
 Builtins.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi
@@ -59,31 +53,21 @@ Machine.cmx: Machine.cmi
 Main.cmo: Parse.cmi GCC.cmi Cprint.cmi Builtins.cmi
 Main.cmx: Parse.cmx GCC.cmx Cprint.cmx Builtins.cmx
 PackedStructs.cmo: Transform.cmi Machine.cmi Errors.cmi Env.cmi Cutil.cmi \
-    C.cmi Builtins.cmi PackedStructs.cmi
+    Cprint.cmi C.cmi Builtins.cmi
 PackedStructs.cmx: Transform.cmx Machine.cmx Errors.cmx Env.cmx Cutil.cmx \
-    C.cmi Builtins.cmx PackedStructs.cmi
-Parse.cmo: Unblock.cmi StructByValue.cmi StructAssign.cmi SimplVolatile.cmo \
-    SimplExpr.cmi Rename.cmi PackedStructs.cmi Errors.cmi Elab.cmi \
-    Bitfields.cmi AddCasts.cmi Parse.cmi
-Parse.cmx: Unblock.cmx StructByValue.cmx StructAssign.cmx SimplVolatile.cmx \
-    SimplExpr.cmx Rename.cmx PackedStructs.cmx Errors.cmx Elab.cmx \
-    Bitfields.cmx AddCasts.cmx Parse.cmi
+    Cprint.cmx C.cmi Builtins.cmx
+Parse.cmo: Unblock.cmi StructReturn.cmi Rename.cmi PackedStructs.cmo \
+    Errors.cmi Elab.cmi Bitfields.cmi Parse.cmi
+Parse.cmx: Unblock.cmx StructReturn.cmx Rename.cmx PackedStructs.cmx \
+    Errors.cmx Elab.cmx Bitfields.cmx Parse.cmi
 Parse_aux.cmo: Errors.cmi Cabshelper.cmo Parse_aux.cmi
 Parse_aux.cmx: Errors.cmx Cabshelper.cmx Parse_aux.cmi
 Parser.cmo: Parse_aux.cmi Cabshelper.cmo Cabs.cmo Parser.cmi
 Parser.cmx: Parse_aux.cmx Cabshelper.cmx Cabs.cmx Parser.cmi
 Rename.cmo: Errors.cmi Cutil.cmi C.cmi Builtins.cmi Rename.cmi
 Rename.cmx: Errors.cmx Cutil.cmx C.cmi Builtins.cmx Rename.cmi
-SimplExpr.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi SimplExpr.cmi
-SimplExpr.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi SimplExpr.cmi
-SimplVolatile.cmo: Transform.cmi Cutil.cmi C.cmi
-SimplVolatile.cmx: Transform.cmx Cutil.cmx C.cmi
-StructAssign.cmo: Transform.cmi Machine.cmi Errors.cmi Env.cmi Cutil.cmi \
-    C.cmi StructAssign.cmi
-StructAssign.cmx: Transform.cmx Machine.cmx Errors.cmx Env.cmx Cutil.cmx \
-    C.cmi StructAssign.cmi
-StructByValue.cmo: Transform.cmi Env.cmi Cutil.cmi C.cmi StructByValue.cmi
-StructByValue.cmx: Transform.cmx Env.cmx Cutil.cmx C.cmi StructByValue.cmi
+StructReturn.cmo: Transform.cmi Env.cmi Cutil.cmi C.cmi StructReturn.cmi
+StructReturn.cmx: Transform.cmx Env.cmx Cutil.cmx C.cmi StructReturn.cmi
 Transform.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi Transform.cmi
 Transform.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmx Transform.cmi
 Unblock.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi Unblock.cmi
diff --git a/cparser/AddCasts.ml b/cparser/AddCasts.ml
deleted file mode 100644
index eb3fa08..0000000
--- a/cparser/AddCasts.ml
+++ /dev/null
@@ -1,243 +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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Materialize implicit casts *)
-
-(* Assumes: simplified code
-   Produces: simplified code
-   Preserves: unblocked code *)
-
-open C
-open Cutil
-open Transform
-
-(* We have the option of materializing all casts or leave "widening"
-   casts implicit.  Widening casts are:
-- from a small integer type to a larger integer type,
-  provided both types have the same signedness;
-- from a small float type to a larger float type;
-- from a pointer type to void *. 
-*)
-
-let omit_widening_casts = ref false
-
-let widening_cast env tfrom tto =
-  begin match unroll env tfrom, unroll env tto with
-  | TInt(k1, _), TInt(k2, _) ->
-      integer_rank k1 <= integer_rank k2
-      && is_signed_ikind k1 = is_signed_ikind k2
-  | TFloat(k1, _), TFloat(k2, _) ->
-      float_rank k1 <= float_rank k2
-  | TPtr(ty1, _), TPtr(ty2, _) -> is_void_type env ty2
-  | _, _ -> false
-  end
-
-let cast_not_needed env tfrom tto =
-  let tfrom = pointer_decay env tfrom
-  and tto = pointer_decay env tto in
-  compatible_types env tfrom tto
-  || (!omit_widening_casts && widening_cast env tfrom tto)
-
-let cast env e tto =
-  if cast_not_needed env e.etyp tto
-  then e
-  else {edesc = ECast(tto, e); etyp = tto}
-
-(* Note: this pass applies only to simplified expressions 
-   because casts cannot be materialized in op= expressions... *)
-
-let rec add_expr env e =
-  match e.edesc with
-  | EConst _ -> e
-  | EVar _ -> e
-  | ESizeof _ -> e
-  | EUnop(op, e1) ->
-      let e1' = add_expr env e1 in
-      let desc =
-        match op with
-        | Ominus | Oplus | Onot ->
-            EUnop(op, cast env e1' e.etyp)
-        | Olognot | Oderef | Oaddrof
-        | Odot _ | Oarrow _ ->
-            EUnop(op, e1')
-        | Opreincr | Opredecr | Opostincr | Opostdecr ->
-            assert false (* not simplified *)
-      in { edesc = desc; etyp = e.etyp }
-  | EBinop(op, e1, e2, ty) ->
-      let e1' = add_expr env e1 in
-      let e2' = add_expr env e2 in
-      let desc =
-        match op with
-        | Oadd ->
-            if is_pointer_type env ty
-            then EBinop(Oadd, e1', e2', ty)
-            else EBinop(Oadd, cast env e1' ty, cast env e2' ty, ty)
-        | Osub ->
-            if is_pointer_type env ty
-            then EBinop(Osub, e1', e2', ty)
-            else EBinop(Osub, cast env e1' ty, cast env e2' ty, ty)
-        | Omul|Odiv|Omod|Oand|Oor|Oxor|Oeq|One|Olt|Ogt|Ole|Oge ->
-            EBinop(op, cast env e1' ty, cast env e2' ty, ty)
-        | Oshl|Oshr ->
-            EBinop(op, cast env e1' ty, e2', ty)
-        | Oindex | Ologand | Ologor | Ocomma ->
-            EBinop(op, e1', e2', ty)
-        | Oassign
-        | Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign
-        | Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign ->
-            assert false (* not simplified *)
-      in { edesc = desc; etyp = e.etyp }
-  | EConditional(e1, e2, e3) ->
-      { edesc = 
-          EConditional(add_expr env e1, add_expr env e2, add_expr env e3);
-        etyp = e.etyp }
-  | ECast(ty, e1) ->
-      { edesc = ECast(ty, add_expr env e1); etyp = e.etyp }
-  | ECall(e1, el) ->
-      assert false (* not simplified *)
-
-(* Arguments to a prototyped function *)
-
-let rec add_proto env args params =
-  match args, params with
-  | [], _ -> []
-  | _::_, [] -> add_noproto env args
-  | arg1 :: argl, (_, ty_p) :: paraml ->
-      cast env (add_expr env arg1) ty_p ::
-      add_proto env argl paraml
-
-(* Arguments to a non-prototyped function *)
-
-and add_noproto env args =
-  match args with
-  | [] -> []
-  | arg1 :: argl ->
-      cast env (add_expr env arg1) (default_argument_conversion env arg1.etyp) ::
-      add_noproto env argl
-
-(* Arguments to function calls in general *)
-
-let add_arguments env ty_fun args =
-  let ty_args =
-    match unroll env ty_fun with
-    | TFun(res, args, vararg, a) -> args
-    | TPtr(ty, a) ->
-        begin match unroll env ty with
-        | TFun(res, args, vararg, a) -> args
-        | _ -> assert false
-        end
-    | _ -> assert false in
-  match ty_args with
-  | None -> add_noproto env args
-  | Some targs -> add_proto env args targs
-
-(* Toplevel expressions (appearing in Sdo statements) *)
-
-let add_topexpr env loc e =
-  match e.edesc with
-  | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty}, _) ->
-      let ecall =
-        {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
-         etyp = ty} in
-      if cast_not_needed env ty lhs.etyp then
-        sassign loc (add_expr env lhs) ecall
-      else begin
-        let tmp = new_temp (erase_attributes_type env ty) in
-        sseq loc (sassign loc tmp ecall) 
-                 (sassign loc (add_expr env lhs) (cast env tmp lhs.etyp))
-      end
-  | EBinop(Oassign, lhs, rhs, _) ->
-      sassign loc (add_expr env lhs) (cast env (add_expr env rhs) lhs.etyp)
-  | ECall(e1, el) ->
-      let ecall =
-        {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
-         etyp = e.etyp} in
-      {sdesc = Sdo ecall; sloc = loc}
-  | _ ->
-      assert false
-
-(* Initializers *)
-
-let rec add_init env tto = function
-  | Init_single e ->
-      Init_single (cast env (add_expr env e) tto)
-  | Init_array il ->
-      let ty_elt =
-        match unroll env tto with
-        | TArray(ty, _, _) -> ty | _ -> assert false in
-      Init_array (List.map (add_init env ty_elt) il)
-  | Init_struct(id, fil) ->
-      Init_struct (id, List.map
-                         (fun (fld, i) -> (fld, add_init env fld.fld_typ i))
-                         fil)
-  | Init_union(id, fld, i) ->
-      Init_union(id, fld, add_init env fld.fld_typ i)
-
-(* Declarations *)
-
-let add_decl env (sto, id, ty, optinit) =
-  (sto, id, ty,
-   begin match optinit with
-         | None -> None
-         | Some init -> Some(add_init env ty init)
-   end)
-
-(* Statements *)
-
-let rec add_stmt env f s =
-  match s.sdesc with
-  | Sskip -> s
-  | Sdo e -> add_topexpr env s.sloc e
-  | Sseq(s1, s2) -> 
-      {sdesc = Sseq(add_stmt env f s1, add_stmt env f s2); sloc = s.sloc }
-  | Sif(e, s1, s2) ->
-      {sdesc = Sif(add_expr env e, add_stmt env f s1, add_stmt env f s2);
-       sloc = s.sloc}
-  | Swhile(e, s1) ->
-      {sdesc = Swhile(add_expr env e, add_stmt env f s1);
-       sloc = s.sloc}
-  | Sdowhile(s1, e) ->
-      {sdesc = Sdowhile(add_stmt env f s1, add_expr env e);
-       sloc = s.sloc}
-  | Sfor(s1, e, s2, s3) ->
-      {sdesc = Sfor(add_stmt env f s1, add_expr env e, add_stmt env f s2,
-                    add_stmt env f s3);
-       sloc = s.sloc}
-  | Sbreak -> s
-  | Scontinue -> s
-  | Sswitch(e, s1) ->
-      {sdesc = Sswitch(add_expr env e, add_stmt env f s1); sloc = s.sloc}
-  | Slabeled(lbl, s) ->
-      {sdesc = Slabeled(lbl, add_stmt env f s); sloc = s.sloc}
-  | Sgoto lbl -> s
-  | Sreturn None -> s
-  | Sreturn (Some e) ->
-      {sdesc = Sreturn(Some(cast env (add_expr env e) f.fd_ret)); sloc = s.sloc}
-  | Sblock sl ->
-      {sdesc = Sblock(List.map (add_stmt env f) sl); sloc = s.sloc}
-  | Sdecl d ->
-      {sdesc = Sdecl(add_decl env d); sloc = s.sloc}
-
-let add_fundef env f =
-  reset_temps();
-  let body' = add_stmt env f f.fd_body in
-  let temps = get_temps () in
-  (* fd_locals have no initializers, so no need to transform them *)
-  { f with fd_locals = f.fd_locals @ temps; fd_body = body' }
-
-
-let program ?(all = false) p =
-  omit_widening_casts := not all;
-  Transform.program ~decl:add_decl ~fundef:add_fundef p
diff --git a/cparser/AddCasts.mli b/cparser/AddCasts.mli
deleted file mode 100644
index 318ecc6..0000000
--- a/cparser/AddCasts.mli
+++ /dev/null
@@ -1,16 +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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-val program: ?all: bool -> C.program -> C.program
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 870385d..2da1936 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1508,13 +1508,13 @@ let rec enter_decdefs local loc env = function
       (* check for incomplete type *)
       if sto' <> Storage_extern && incomplete_type env ty' then
         warning loc "'%s' has incomplete type" s;
-      if local && sto <> Storage_extern && sto <> Storage_static then begin
+      if local && sto' <> Storage_extern && sto' <> Storage_static then begin
         (* Local definition *)
         let (decls, env3) = enter_decdefs local loc env2 rem in
         ((sto', id, ty', init') :: decls, env3)
       end else begin
         (* Global definition *)
-        emit_elab (elab_loc loc) (Gdecl(sto, id, ty', init'));
+        emit_elab (elab_loc loc) (Gdecl(sto', id, ty', init'));
         enter_decdefs local loc env2 rem
       end
 
diff --git a/cparser/Makefile b/cparser/Makefile
index 527cdd3..da2c28b 100644
--- a/cparser/Makefile
+++ b/cparser/Makefile
@@ -15,8 +15,8 @@ SRCS=Errors.ml Cabs.ml Cabshelper.ml Parse_aux.ml Parser.ml Lexer.ml \
   Builtins.ml GCC.ml \
   Cleanup.ml Elab.ml Rename.ml \
   Transform.ml \
-  Unblock.ml SimplExpr.ml AddCasts.ml StructByValue.ml StructAssign.ml \
-  Bitfields.ml PackedStructs.ml SimplVolatile.ml \
+  Unblock.ml StructReturn.ml \
+  Bitfields.ml PackedStructs.ml \
   Parse.ml
 
 COBJS=uint64.o
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index dcd01e9..2c467a7 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -20,28 +20,18 @@ module CharSet = Set.Make(struct type t = char let compare = compare end)
 let transform_program t p =
   let run_pass pass flag p = if CharSet.mem flag t then pass p else p in
   Rename.program
-  (run_pass (AddCasts.program ~all:(CharSet.mem 'C' t)) 'c'
-  (run_pass (SimplExpr.program ~volatile:(CharSet.mem 'V' t)) 'e'
-  (run_pass SimplVolatile.program 'v'
-  (run_pass StructAssign.program 'S'
-  (run_pass StructByValue.program 's'
+  (run_pass StructReturn.program 's'
   (run_pass PackedStructs.program 'p'
   (run_pass Bitfields.program 'f'
   (run_pass Unblock.program 'b'
-  p))))))))
+  p))))
 
 let parse_transformations s =
   let t = ref CharSet.empty in
   let set s = String.iter (fun c -> t := CharSet.add c !t) s in
   String.iter
     (function 'b' -> set "b"
-            | 'e' -> set "e"
-            | 'c' -> set "ec"
-            | 'C' -> set "ecC"
             | 's' -> set "s"
-            | 'S' -> set "bsS"
-            | 'v' -> set "v"
-            | 'V' -> set "eV"
             | 'f' -> set "bf"
             | 'p' -> set "bp"
             |  _  -> ())
diff --git a/cparser/SimplExpr.ml b/cparser/SimplExpr.ml
deleted file mode 100644
index 4184d95..0000000
--- a/cparser/SimplExpr.ml
+++ /dev/null
@@ -1,568 +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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Pulling side-effects out of expressions *)
-
-(* Assumes: nothing
-   Produces: simplified code *)
-
-open C
-open Cutil
-open Transform
-
-(* Grammar of simplified expressions:
-      e ::= EConst cst
-          | ESizeof ty
-          | EVar id
-          | EUnop pure-unop e
-          | EBinop pure-binop e e
-          | EConditional e e e
-          | ECast ty e
-
-   Grammar of statements produced to reflect side-effects in expressions:
-      s ::= Sskip
-          | Sdo (EBinop Oassign e e)
-          | Sdo (EBinop Oassign e (ECall e e* ))
-          | Sdo (Ecall e el)
-          | Sseq s s
-          | Sif e s s
-*)
-
-let rec is_simpl_expr e =
-  match e.edesc with
-  | EConst cst -> true
-  | ESizeof ty -> true
-  | EVar id -> true
-  | EUnop((Ominus|Oplus|Olognot|Onot|Oderef|Oaddrof), e1) ->
-      is_simpl_expr e1
-  | EBinop((Oadd|Osub|Omul|Odiv|Omod|Oand|Oor|Oxor|Oshl|Oshr|
-            Oeq|One|Olt|Ogt|Ole|Oge|Oindex|Ologand|Ologor), e1, e2, _) ->
-      is_simpl_expr e1 && is_simpl_expr e2
-  | EConditional(e1, e2, e3) ->
-      is_simpl_expr e1 && is_simpl_expr e2 && is_simpl_expr e3
-  | ECast(ty, e1) ->
-      is_simpl_expr e1
-  | _ ->
-      false
-
-(* "Destination" of a simplified expression *)
-
-type exp_destination =
-  | RHS                  (* evaluate as a r-value *)
-  | LHS                  (* evaluate as a l-value *)
-  | Drop                 (* drop its value, we only need the side-effects *)
-  | Set of exp           (* assign it to the given simplified l.h.s. *)
-
-let voidconst = { nullconst with etyp = TVoid [] }
-
-(* Reads from volatile lvalues are also considered as side-effects if
-   [volatilize] is true. *)
-
-let volatilize = ref false
-
-(* [simpl_expr loc env e act] returns a pair [s, e'] of
-   a statement that performs the side-effects present in [e] and
-   a simplified, side-effect-free expression [e'].
-   If [act] is [RHS], [e'] evaluates to the same value as [e].
-   If [act] is [LHS], [e'] evaluates to the same location as [e].
-   If [act] is [Drop], [e'] is not meaningful and must be ignored.
-   If [act] is [Set lhs], [s] also performs an assignment
-   equivalent to [lhs = e].  [e'] is not meaningful. *)
-
-let simpl_expr loc env e act =
-
-  (* Temporaries should not be [const] because we assign into them,
-     and need not be [volatile] because no one else is writing into them.
-     As for [restrict] it doesn't make sense anyway. *)
-
-  let new_temp ty =
-    Transform.new_temp (erase_attributes_type env ty) in
-
-  let eboolvalof e =
-    { edesc = EBinop(One, e, intconst 0L IInt, TInt(IInt, []));
-      etyp = TInt(IInt, []) } in
-
-  let sseq s1 s2 = Cutil.sseq loc s1 s2 in
-
-  let sassign e1 e2 =
-    { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp}; 
-      sloc = loc } in
-
-  let sif e s1 s2 =
-    { sdesc = Sif(e, s1, s2); sloc = loc } in
-
-  let is_volatile_read e =
-    !volatilize
-    && List.mem AVolatile (attributes_of_type env e.etyp)
-    && is_lvalue e in
-
-  let lhs_to_rhs e =
-    if is_volatile_read e
-    then (let t = new_temp e.etyp in (sassign t e, t))
-    else (sskip, e) in
-
-  let finish act s e =
-    match act with
-    | RHS ->
-        if is_volatile_read e
-        then (let t = new_temp e.etyp in (sseq s (sassign t e), t))
-        else (s, e)
-    | LHS ->
-        (s, e)
-    | Drop -> 
-        if is_volatile_read e
-        then (let t = new_temp e.etyp in (sseq s (sassign t e), voidconst))
-        else (s, voidconst)
-    | Set lhs ->
-        if is_volatile_read e
-        then (let t = new_temp e.etyp in
-                 (sseq s (sseq (sassign t e) (sassign lhs t)), voidconst))
-        else (sseq s (sassign lhs e), voidconst) in
-
-   let rec simpl e act =
-    match e.edesc with
-
-    | EConst cst -> 
-        finish act sskip e
-
-    | ESizeof ty -> 
-        finish act sskip e
-
-    | EVar id ->
-        finish act sskip e
-
-    | EUnop(op, e1) ->
-
-        begin match op with
-
-        | Ominus | Oplus | Olognot | Onot | Oderef | Oarrow _ ->
-            let (s1, e1') = simpl e1 RHS in
-            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
-
-        | Oaddrof ->
-            let (s1, e1') = simpl e1 LHS in
-            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
-
-        | Odot _ ->
-            let (s1, e1') = simpl e1 (if act = LHS then LHS else RHS) in
-            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
-
-        | Opreincr | Opredecr ->
-            let (s1, e1') = simpl e1 LHS in
-            let (s2, e2') = lhs_to_rhs e1' in
-            let op' = match op with Opreincr -> Oadd | _ -> Osub in
-            let ty = unary_conversion env e.etyp in
-            let e3 =
-              {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
-            begin match act with
-            | Drop ->
-                (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
-            | _ ->
-                let tmp = new_temp e.etyp in
-                finish act (sseq s1 (sseq s2 (sseq (sassign tmp e3)
-                                                   (sassign e1' tmp))))
-                       tmp
-            end
-
-        | Opostincr | Opostdecr ->
-            let (s1, e1') = simpl e1 LHS in
-            let op' = match op with Opostincr -> Oadd | _ -> Osub in
-            let ty = unary_conversion env e.etyp in
-            begin match act with
-            | Drop ->
-                let (s2, e2') = lhs_to_rhs e1' in
-                let e3 =
-                  {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
-                (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
-            | _ ->
-                let tmp = new_temp e.etyp in
-                let e3 =
-                  {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty} in
-                finish act (sseq s1 (sseq (sassign tmp e1') (sassign e1' e3))) 
-                       tmp
-            end
-
-        end
-
-    | EBinop(op, e1, e2, ty) ->
-
-        begin match op with
-
-        | Oadd | Osub | Omul | Odiv | Omod | Oand | Oor | Oxor
-        | Oshl | Oshr | Oeq | One | Olt | Ogt | Ole | Oge | Oindex ->
-            let (s1, e1') = simpl e1 RHS in
-            let (s2, e2') = simpl e2 RHS in
-            finish act (sseq s1 s2)
-                       {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp}
-
-        | Oassign ->
-            if act = Drop && is_simpl_expr e1 then
-              simpl e2 (Set e1)
-            else begin
-              match act with
-              | Drop ->
-                  let (s1, e1') = simpl e1 LHS in
-                  let (s2, e2') = simpl e2 RHS in
-                  (sseq s1 (sseq s2 (sassign e1' e2')), voidconst)
-              | _ ->
-                  let tmp = new_temp e.etyp in
-                  let (s1, e1') = simpl e1 LHS in
-                  let (s2, e2') = simpl e2 (Set tmp) in
-                  finish act (sseq s1 (sseq s2 (sassign e1' tmp)))
-                             tmp
-            end
-
-        | Oadd_assign | Osub_assign | Omul_assign | Odiv_assign
-        | Omod_assign | Oand_assign | Oor_assign  | Oxor_assign
-        | Oshl_assign | Oshr_assign ->
-            let (s1, e1') = simpl e1 LHS in
-            let (s11, e11') = lhs_to_rhs e1' in
-            let (s2, e2') = simpl e2 RHS in
-            let op' =
-              match op with
-              | Oadd_assign -> Oadd    | Osub_assign -> Osub
-              | Omul_assign -> Omul    | Odiv_assign -> Odiv
-              | Omod_assign -> Omod    | Oand_assign -> Oand
-              | Oor_assign  -> Oor     | Oxor_assign -> Oxor
-              | Oshl_assign -> Oshl    | Oshr_assign -> Oshr
-              | _ -> assert false in
-            let e3 =
-              { edesc = EBinop(op', e11', e2', ty); etyp = ty } in
-            begin match act with
-            | Drop ->
-                (sseq s1 (sseq s11 (sseq s2 (sassign e1' e3))), voidconst)
-            | _ ->
-                let tmp = new_temp e.etyp in
-                finish act (sseq s1 (sseq s11 (sseq s2
-                               (sseq (sassign tmp e3) (sassign e1' tmp)))))
-                           tmp
-            end
-
-        | Ocomma ->
-            let (s1, _) = simpl e1 Drop in
-            let (s2, e2') = simpl e2 act in
-            (sseq s1 s2, e2')
-
-        | Ologand ->
-            let (s1, e1') = simpl e1 RHS in
-            if is_simpl_expr e2 then begin
-              finish act s1
-                     {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp}
-            end else begin
-              match act with
-              | Drop ->
-                  let (s2, _) = simpl e2 Drop in
-                  (sseq s1 (sif e1' s2 sskip), voidconst)
-              | RHS | LHS ->  (* LHS should not happen *)
-                  let (s2, e2') = simpl e2 RHS in
-                  let tmp = new_temp e.etyp in
-                  (sseq s1 (sif e1' 
-                              (sseq s2 (sassign tmp (eboolvalof e2')))
-                              (sassign tmp (intconst 0L IInt))),
-                   tmp)
-              | Set lv ->
-                  let (s2, e2') = simpl e2 RHS in
-                  (sseq s1 (sif e1' 
-                              (sseq s2 (sassign lv (eboolvalof e2')))
-                              (sassign lv (intconst 0L IInt))),
-                   voidconst)
-            end             
-
-        | Ologor ->
-            let (s1, e1') = simpl e1 RHS in
-            if is_simpl_expr e2 then begin
-              finish act s1
-                     {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp}
-            end else begin
-              match act with
-              | Drop ->
-                  let (s2, _) = simpl e2 Drop in
-                  (sseq s1 (sif e1' sskip s2), voidconst)
-              | RHS | LHS ->  (* LHS should not happen *)
-                  let (s2, e2') = simpl e2 RHS in
-                  let tmp = new_temp e.etyp in
-                  (sseq s1 (sif e1' 
-                              (sassign tmp (intconst 1L IInt))
-                              (sseq s2 (sassign tmp (eboolvalof e2')))),
-                   tmp)
-              | Set lv ->
-                  let (s2, e2') = simpl e2 RHS in
-                  (sseq s1 (sif e1' 
-                              (sassign lv (intconst 1L IInt))
-                              (sseq s2 (sassign lv (eboolvalof e2')))),
-                   voidconst)
-            end             
-
-        end
-
-    | EConditional(e1, e2, e3) ->
-        let (s1, e1') = simpl e1 RHS in
-        if is_simpl_expr e2 && is_simpl_expr e3 then begin
-          finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp}
-        end else begin
-          match act with
-          | Drop ->
-              let (s2, _) = simpl e2 Drop in
-              let (s3, _) = simpl e3 Drop in
-              (sseq s1 (sif e1' s2 s3), voidconst)
-          | RHS | LHS ->  (* LHS should not happen *)
-              let tmp = new_temp e.etyp in
-              let (s2, _) = simpl e2 (Set tmp) in
-              let (s3, _) = simpl e3 (Set tmp) in
-              (sseq s1 (sif e1' s2 s3), tmp)
-          | Set lv ->
-              let (s2, _) = simpl e2 (Set lv) in
-              let (s3, _) = simpl e3 (Set lv) in
-              (sseq s1 (sif e1' s2 s3), voidconst)
-        end
-
-    | ECast(ty, e1) ->
-        if is_void_type env ty then begin
-          if act <> Drop then
-            Errors.warning "%acast to 'void' in a context expecting a value\n"
-                           formatloc loc;
-            simpl e1 act
-        end else begin
-          let (s1, e1') = simpl e1 RHS in
-          finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp}
-        end
-
-    | ECall(e1, el) ->
-        let (s1, e1') = simpl e1 RHS in
-        let (s2, el') = simpl_list el in
-        let e2 = { edesc = ECall(e1', el'); etyp = e.etyp } in
-        begin match act with
-        | Drop ->
-            (sseq s1 (sseq s2 {sdesc = Sdo e2; sloc=loc}), voidconst)
-        | Set({edesc = EVar _} as lhs) ->
-            (* CompCert wants the destination of a call to be a variable,
-               not a more complex lhs.  In the latter case, we
-               fall through the catch-all case below *)
-            (sseq s1 (sseq s2 (sassign lhs e2)), voidconst)
-        | _ ->
-            let tmp = new_temp e.etyp in
-            finish act (sseq s1 (sseq s2 (sassign tmp e2))) tmp
-        end
-
-  and simpl_list = function
-    | [] -> (sskip, [])
-    | e1 :: el ->
-        let (s1, e1') = simpl e1 RHS in
-        let (s2, el') = simpl_list el in
-        (sseq s1 s2, e1' :: el')
-
-  in simpl e act
-
-(* Simplification of an initializer *)
-
-let simpl_initializer loc env i =
-
-  let rec simpl_init = function
-  | Init_single e ->
-      let (s, e') = simpl_expr loc env e RHS in
-      (s, Init_single e)
-  | Init_array il ->
-      let rec simpl = function
-      | [] -> (sskip, [])
-      | i1 :: il ->
-          let (s1, i1') = simpl_init i1 in
-          let (s2, il') = simpl il in
-          (sseq loc s1 s2, i1' :: il') in
-      let (s, il') = simpl il in
-      (s, Init_array il')
-  | Init_struct(id, il) ->
-      let rec simpl = function
-      | [] -> (sskip, [])
-      | (f1, i1) :: il ->
-          let (s1, i1') = simpl_init i1 in
-          let (s2, il') = simpl il in
-          (sseq loc s1 s2, (f1, i1') :: il') in
-      let (s, il') = simpl il in
-      (s, Init_struct(id, il'))
-  | Init_union(id, f, i) ->
-      let (s, i') = simpl_init i in
-      (s, Init_union(id, f, i'))
-
-  in simpl_init i
-
-(* Construct a simplified statement equivalent to [if (e) s1; else s2;].
-   Optimizes the case where e contains [&&] or [||] or [?].
-   [s1] or [s2] can be duplicated, so use only for small [s1] and [s2]
-   that do not define any labels. *)
-
-let rec simpl_if loc env e s1 s2 =
-  match e.edesc with
-  | EUnop(Olognot, e1) ->
-      simpl_if loc env e1 s2 s1
-  | EBinop(Ologand, e1, e2, _) ->
-      simpl_if loc env e1
-        (simpl_if loc env e2 s1 s2)
-        s2
-  | EBinop(Ologor, e1, e2, _) ->
-      simpl_if loc env e1
-        s1
-        (simpl_if loc env e2 s1 s2)
-  | EConditional(e1, e2, e3) ->
-      simpl_if loc env e1
-        (simpl_if loc env e2 s1 s2)
-        (simpl_if loc env e3 s1 s2)
-  | _ ->
-      let (s, e') = simpl_expr loc env e RHS in
-      sseq loc s {sdesc = Sif(e', s1, s2); sloc = loc}
-
-(* Trivial statements for which [simpl_if] is applicable *)
-
-let trivial_stmt s =
-  match s.sdesc with
-  | Sskip | Scontinue | Sbreak | Sgoto _ -> true
-  | _ -> false
-
-(* Construct a simplified statement equivalent to [if (!e) exit; ]. *)
-
-let break_if_false loc env e =
-  simpl_if loc env e
-           {sdesc = Sskip; sloc = loc}
-           {sdesc = Sbreak; sloc = loc}
-
-(* Simplification of a statement *)
-
-let simpl_statement env s =
-
-  let rec simpl_stmt s =
-    match s.sdesc with
-
-  | Sskip ->
-      s
-
-  | Sdo e ->
-      let (s', _) = simpl_expr s.sloc env e Drop in
-      s'
-
-  | Sseq(s1, s2) ->
-      {sdesc = Sseq(simpl_stmt s1, simpl_stmt s2); sloc = s.sloc}
-
-  | Sif(e, s1, s2) ->
-      if trivial_stmt s1 && trivial_stmt s2 then
-        simpl_if s.sloc env e (simpl_stmt s1) (simpl_stmt s2)
-      else begin
-        let (s', e') = simpl_expr s.sloc env e RHS in
-        sseq s.sloc s'
-          {sdesc = Sif(e', simpl_stmt s1, simpl_stmt s2);
-           sloc = s.sloc}
-      end
-
-  | Swhile(e, s1) ->
-      if is_simpl_expr e then
-        {sdesc = Swhile(e, simpl_stmt s1); sloc = s.sloc}
-      else
-        {sdesc =
-           Swhile(intconst 1L IInt,
-                  sseq s.sloc (break_if_false s.sloc env e)
-                              (simpl_stmt s1));
-         sloc = s.sloc}
-
-  | Sdowhile(s1, e) ->
-      if is_simpl_expr e then
-        {sdesc = Sdowhile(simpl_stmt s1, e); sloc = s.sloc}
-      else begin
-        let tmp = new_temp (TInt(IInt, [])) in
-        let (s', _) = simpl_expr s.sloc env e (Set tmp) in
-        let s_init =
-          {sdesc = Sdo {edesc = EBinop(Oassign, tmp, intconst 1L IInt, tmp.etyp);
-                        etyp = tmp.etyp};
-           sloc = s.sloc} in
-        {sdesc = Sfor(s_init, tmp, s', simpl_stmt s1); sloc = s.sloc}
-      end
-(*** Alternate translation that unfortunately puts a "break" in the
-     "next" part of a "for", something that is not supported
-     by Clight semantics, and has unknown behavior in gcc.
-        {sdesc =
-           Sfor(sskip, 
-                intconst 1L IInt,
-                break_if_false s.sloc env e,
-                simpl_stmt s1);
-         sloc = s.sloc}
-***)
-
-  | Sfor(s1, e, s2, s3) ->
-      if is_simpl_expr e then
-        {sdesc = Sfor(simpl_stmt s1,
-                      e,
-                      simpl_stmt s2,
-                      simpl_stmt s3);
-         sloc = s.sloc}
-      else
-        let (s', e') = simpl_expr s.sloc env e RHS in
-        {sdesc = Sfor(sseq s.sloc (simpl_stmt s1) s',
-                      e',
-                      sseq s.sloc (simpl_stmt s2) s',
-                      simpl_stmt s3);
-         sloc = s.sloc}
-
-  | Sbreak ->
-      s
-  | Scontinue ->
-      s
-
-  | Sswitch(e, s1) ->
-      let (s', e') = simpl_expr s.sloc env e RHS in
-      sseq s.sloc s' {sdesc = Sswitch(e', simpl_stmt s1); sloc = s.sloc}
-
-  | Slabeled(lbl, s1) ->
-      {sdesc = Slabeled(lbl, simpl_stmt s1); sloc = s.sloc}
-
-  | Sgoto lbl ->
-      s
-
-  | Sreturn None ->
-      s
-
-  | Sreturn (Some e) ->
-      let (s', e') = simpl_expr s.sloc env e RHS in
-      sseq s.sloc s' {sdesc = Sreturn(Some e'); sloc = s.sloc}
-
-  | Sblock sl ->
-      {sdesc = Sblock(simpl_block sl); sloc = s.sloc}
-
-  | Sdecl d -> assert false
-
-  and simpl_block = function
-  | [] -> []
-  | ({sdesc = Sdecl(sto, id, ty, None)} as s) :: sl ->
-      s :: simpl_block sl
-  | ({sdesc = Sdecl(sto, id, ty, Some i)} as s) :: sl ->
-      let (s', i') = simpl_initializer s.sloc env i in
-      let sl' =
-           {sdesc = Sdecl(sto, id, ty, Some i'); sloc = s.sloc}
-        :: simpl_block sl in
-      if s'.sdesc = Sskip then sl' else s' :: sl'
-  | s :: sl ->
-      simpl_stmt s :: simpl_block sl
-
-  in simpl_stmt s
-
-(* Simplification of a function definition *)
-
-let simpl_fundef env f =
-  reset_temps();
-  let body' = simpl_statement env f.fd_body in
-  let temps = get_temps() in
-  { f with fd_locals = f.fd_locals @ temps; fd_body = body' }
-
-(* Entry point *)
-
-let program ?(volatile = false) p =
-  volatilize := volatile;
-  Transform.program ~fundef:simpl_fundef p
diff --git a/cparser/SimplExpr.mli b/cparser/SimplExpr.mli
deleted file mode 100644
index cdeb30c..0000000
--- a/cparser/SimplExpr.mli
+++ /dev/null
@@ -1,20 +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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Pulling side effects out of expressions.
-   If [volatile] is [true], treats reads from volatile rvalues 
-   as side-effects *)
-
-val program: ?volatile: bool -> C.program -> C.program
diff --git a/cparser/SimplVolatile.ml b/cparser/SimplVolatile.ml
deleted file mode 100644
index ef7a3a0..0000000
--- 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
diff --git a/cparser/StructAssign.ml b/cparser/StructAssign.ml
deleted file mode 100644
index d9ad8f5..0000000
--- a/cparser/StructAssign.ml
+++ /dev/null
@@ -1,165 +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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Expand assignments between structs and between unions *)
-
-(* Assumes: unblocked code.
-   Preserves: unblocked code *)
-
-open C
-open Machine
-open Cutil
-open Env
-open Errors
-open Transform
-
-(* Finding appropriate memcpy functions *)
-
-let memcpy_decl = ref (None : ident option)
-
-let memcpy_type =
-  TFun(TPtr(TVoid [], []),
-       Some [(Env.fresh_ident "", TPtr(TVoid [], []));
-             (Env.fresh_ident "", TPtr(TVoid [AConst], []));
-             (Env.fresh_ident "", TInt(size_t_ikind, []))],
-       false, [])
-
-let lookup_function env name =
-  match Env.lookup_ident env name with
-  | (id, II_ident(sto, ty)) -> (id, ty)
-  | (id, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name))
-
-let default_memcpy () =
-  match !memcpy_decl with
-  | Some id ->
-      (id, memcpy_type)
-  | None ->
-      let id = Env.fresh_ident "memcpy" in
-      memcpy_decl := Some id;
-      (id, memcpy_type)
-
-let find_memcpy env =
-  try
-    (lookup_function env "__builtin_memcpy_aligned", true)
-  with Env.Error _ ->
-  try
-    (lookup_function env "__builtin_memcpy", false)
-  with Env.Error _ ->
-  try
-    (lookup_function env "memcpy", false)
-  with Env.Error _ ->
-    (default_memcpy(), false)
-
-(* Smart constructor that "bubble up" sequence expressions *)
-
-let rec edot f e ty =
-  match e.edesc with
-  | EBinop(Ocomma, e1, e2, _) -> ecomma e1 (edot f e2 ty)
-  | _ -> { edesc = EUnop(Odot f, e); etyp = ty }
-
-(* Translate an assignment [lhs = rhs] between composite types.
-   [lhs] and [rhs] must be l-values. *)
-
-let transf_assign env lhs rhs =
-  let al =
-     match Cutil.alignof env lhs.etyp with Some al -> al | None -> 1 in
-  let ((ident, ty), four_args) = find_memcpy env in
-  let memcpy = {edesc = EVar(ident); etyp = ty} in
-  let e_lhs = eaddrof lhs
-  and e_rhs = eaddrof rhs
-  and e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])}
-  and e_align = intconst (Int64.of_int al) size_t_ikind in
-  let args =
-    if four_args
-    then [e_lhs; e_rhs; e_size; e_align]
-    else [e_lhs; e_rhs; e_size] in
-  {edesc = ECall(memcpy, args); etyp = TVoid[]}
-
-(* Transformation of expressions. *)
-
-let transf_expr loc env ctx e =
-  let rec texp ctx e =
-  match e.edesc with
-  | EBinop(Oassign, lhs, rhs, _) when is_composite_type env lhs.etyp ->
-      let lhs' = texp Val lhs in
-      let rhs' = texp Val rhs in
-      begin match ctx with
-      | Effects ->
-          transf_assign env lhs' rhs'
-      | Val ->
-          bind_lvalue env lhs' (fun l -> ecomma (transf_assign env l rhs') l)
-      end
-  | EConst c -> e
-  | ESizeof ty -> e
-  | EVar x ->
-      if ctx = Effects && is_composite_type env e.etyp
-      then nullconst
-      else e
-  | EUnop(Oaddrof, e1) ->
-      eaddrof (texp Val e1)
-  | EUnop(Oderef, e1) ->
-      if ctx = Effects && is_composite_type env e.etyp
-      then texp Effects e1
-      else {edesc = EUnop(Oderef, texp Val e1); etyp = e.etyp}
-  | EUnop(Odot f, e1) ->
-      if ctx = Effects && is_composite_type env e.etyp
-      then texp Effects e1
-      else edot f (texp Val e1) e.etyp
-  | EUnop(Oarrow f, e1) ->
-      if ctx = Effects && is_composite_type env e.etyp
-      then texp Effects e1
-      else {edesc = EUnop(Oarrow f, texp Val e1); etyp = e.etyp}
-  | EUnop(op, e1) ->
-      {edesc = EUnop(op, texp Val e1); etyp = e.etyp}
-  | EBinop(Oindex, e1, e2, ty) ->
-      if ctx = Effects && is_composite_type env e.etyp
-      then ecomma (texp Effects e1) (texp Effects e2)
-      else {edesc = EBinop(Oindex, texp Val e1, texp Val e2, ty); etyp = e.etyp}
-  | EBinop(Ocomma, e1, e2, ty) ->
-      ecomma (texp Effects e1) (texp ctx e2)
-  | 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
-
-(* Transformation of statements *)
-
-let transf_stmt env s =
-  Transform.stmt transf_expr env s
-
-(* Transformation of function definitions *)
-
-let transf_fundef env f =
-  Transform.fundef transf_stmt env f
-
-(* Transformation of programs *)
-
-let program p =
-  memcpy_decl := None;
-  let p' = Transform.program ~fundef:transf_fundef p in
-  match !memcpy_decl with
-  | None -> p'
-  | Some id ->
-      {gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc}
-      :: p'
diff --git a/cparser/StructAssign.mli b/cparser/StructAssign.mli
deleted file mode 100644
index 5549282..0000000
--- a/cparser/StructAssign.mli
+++ /dev/null
@@ -1,18 +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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Expand assignments between structs and between unions *)
-
-val program: C.program -> C.program
diff --git a/cparser/StructByValue.ml b/cparser/StructReturn.ml
index 1b74ec5..2a4bbc1 100644
--- a/cparser/StructByValue.ml
+++ b/cparser/StructReturn.ml
@@ -13,17 +13,14 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(* Eliminate by-value passing of structs and unions. *)
-
-(* Assumes: nothing.
-   Preserves: unblocked code *)
+(* Eliminate structs and unions being returned by value as function results *)
+(* This is a simpler special case of [StructByValue]. *)
 
 open C
 open Cutil
 open Transform
 
-(* In function argument types, struct s -> const struct s *
-   In function result types, struct s -> void + add 1st parameter struct s *
+(* In function result types, struct s -> void + add 1st parameter struct s *
    Try to preserve original typedef names when no change.
 *)
 
@@ -49,11 +46,7 @@ let rec transf_type env t =
       if t1' = t1 then t else TArray(transf_type env t1, sz, attr)
   | _ -> t
 
-and transf_funarg env (id, t) =
-  let t = transf_type env t in
-  if is_composite_type env t
-  then (id, TPtr(add_attributes_type [AConst] t, []))
-  else (id, t)
+and transf_funarg env (id, t) = (id, transf_type env t)
 
 (* Expressions: transform calls + rewrite the types *)
 
@@ -92,26 +85,21 @@ let rec transf_expr env ctx e =
       if is_composite_type env e.etyp then
         transf_composite_call env ctx None fn args e.etyp
       else
-        {edesc = ECall(transf_expr env Val fn, List.map (transf_arg env) args);
+        {edesc = ECall(transf_expr env Val fn,
+                       List.map (transf_expr env Val) args);
          etyp = newty}
 
-(* Function arguments: pass by reference those having composite type *)
-
-and transf_arg env e =
-  let e' = transf_expr env Val e in
-  if is_composite_type env e'.etyp then eaddrof e' else e'
-
 (* Function calls returning a composite: add first argument.
-    ctx = Effects:   lv = f(...)     -> f(&lv, ...)
+    ctx = Effects:   lv = f(...)     -> f(&lv, ...)      [copy optimization]
                      f(...)          -> f(&newtemp, ...)
-    ctx = Val:       lv = f(...)     -> f(&newtemp, ...), lv = newtemp, newtemp
+    ctx = Val:       lv = f(...)     -> f(&newtemp, ...), lv = newtemp
                      f(...)          -> f(&newtemp, ...), newtemp
 *)
 
 and transf_composite_call env ctx opt_lhs fn args ty =
   let ty = transf_type env ty in
   let fn = transf_expr env Val fn in
-  let args = List.map (transf_arg env) args in
+  let args = List.map (transf_expr env Val) args in
   match ctx, opt_lhs with
   | Effects, None ->
       let tmp = new_temp ~name:"_res" ty in
@@ -125,54 +113,14 @@ and transf_composite_call env ctx opt_lhs fn args ty =
   | Val, Some lhs ->
       let lhs = transf_expr env Val lhs in
       let tmp = new_temp ~name:"_res" ty in
-      ecomma (ecomma {edesc = ECall(fn, eaddrof tmp :: args); etyp = TVoid []}
-                     (eassign lhs tmp))
-             tmp
-
-(* The transformation above can create ill-formed lhs containing ",", as in
-     f().x = y    --->   (f(&tmp), tmp).x = y
-     f(g(x));     --->   f(&(g(&tmp),tmp))
-   We fix this by floating the "," above the lhs, up to the nearest enclosing
-   rhs:
-     f().x = y    --->   (f(&tmp), tmp).x = y   --> f(&tmp), tmp.x = y
-     f(g(x));     --->   f(&(g(&tmp),tmp))      --> f((g(&tmp), &tmp))
-*)
-
-let rec float_comma e =
-  match e.edesc with
-  | EConst c -> e
-  | ESizeof ty -> e
-  | EVar x -> e
-  (* lvalue-consuming unops *)
-  | EUnop((Oaddrof|Opreincr|Opredecr|Opostincr|Opostdecr|Odot _) as op,
-          {edesc = EBinop(Ocomma, e1, e2, _)}) ->
-      ecomma (float_comma e1)
-             (float_comma {edesc = EUnop(op, e2); etyp = e.etyp})
-  (* lvalue-consuming binops *)
-  | EBinop((Oassign|Oadd_assign|Osub_assign|Omul_assign|Odiv_assign
-                   |Omod_assign|Oand_assign|Oor_assign|Oxor_assign
-                   |Oshl_assign|Oshr_assign) as op,
-           {edesc = EBinop(Ocomma, e1, e2, _)}, e3, tyres) ->
-      ecomma (float_comma e1)
-             (float_comma {edesc = EBinop(op, e2, e3, tyres); etyp = e.etyp})
-  (* other expressions *)
-  | EUnop(op, e1) ->
-      {edesc = EUnop(op, float_comma e1); etyp = e.etyp}
-  | EBinop(op, e1, e2, tyres) ->
-      {edesc = EBinop(op, float_comma e1, float_comma e2, tyres); etyp = e.etyp}
-  | EConditional(e1, e2, e3) ->
-      {edesc = EConditional(float_comma e1, float_comma e2, float_comma e3);
-       etyp = e.etyp}
-  | ECast(ty, e1) ->
-      {edesc = ECast(ty, float_comma e1); etyp = e.etyp}
-  | ECall(e1, el) ->
-      {edesc = ECall(float_comma e1, List.map float_comma el); etyp = e.etyp}
+      ecomma {edesc = ECall(fn, eaddrof tmp :: args); etyp = TVoid []}
+             (eassign lhs tmp)
 
 (* Initializers *)
 
 let rec transf_init env = function
   | Init_single e ->
-      Init_single (float_comma(transf_expr env Val e))
+      Init_single (transf_expr env Val e)
   | Init_array il ->
       Init_array (List.map (transf_init env) il)
   | Init_struct(id, fil) ->
@@ -190,7 +138,7 @@ let transf_decl env (sto, id, ty, init) =
 
 let transf_funbody env body optres =
 
-let transf_expr ctx e = float_comma(transf_expr env ctx e) in
+let transf_expr ctx e = transf_expr env ctx e in
 
 (* Function returns: if return type is struct or union,
      return x      -> _res = x; return
@@ -239,33 +187,11 @@ let rec transf_stmt s =
 in
   transf_stmt body
 
-let transf_params loc env params =
-  let rec transf_prm = function
-  | [] ->
-      ([], [], sskip)
-  | (id, ty) :: params ->
-      let ty = transf_type env ty in
-      if is_composite_type env ty then begin
-        let id' = Env.fresh_ident id.name in
-        let ty' = TPtr(add_attributes_type [AConst] ty, []) in
-        let (params', decls, init) = transf_prm params in
-        ((id', ty') :: params',
-         (Storage_default, id, ty, None) :: decls,
-         sseq loc
-          (sassign loc {edesc = EVar id; etyp = ty}
-                       {edesc = EUnop(Oderef, {edesc = EVar id'; etyp = ty'});
-                        etyp = ty})
-          init)
-      end else begin
-        let (params', decls, init) = transf_prm params in
-        ((id, ty) :: params', decls, init)
-      end
-  in transf_prm params
-
 let transf_fundef env f =
   reset_temps();
   let ret = transf_type env f.fd_ret in
-  let (params, newdecls, init) = transf_params f.fd_body.sloc env f.fd_params in
+  let params =
+    List.map (fun (id, ty) -> (id, transf_type env ty)) f.fd_params in
   let (ret1, params1, body1) =
     if is_composite_type env ret then begin
       let vres = Env.fresh_ident "_res" in
@@ -277,10 +203,9 @@ let transf_fundef env f =
        transf_funbody env f.fd_body (Some eeres))
     end else
       (ret, params, transf_funbody env f.fd_body None) in
-  let body2 = sseq body1.sloc init body1 in
   let temps = get_temps() in
   {f with fd_ret = ret1; fd_params = params1;
-          fd_locals = newdecls @ f.fd_locals @ temps; fd_body = body2}
+          fd_locals = f.fd_locals @ temps; fd_body = body1}
 
 (* Composites *)
 
diff --git a/cparser/StructByValue.mli b/cparser/StructReturn.mli
index 45899a4..45899a4 100644
--- a/cparser/StructByValue.mli
+++ b/cparser/StructReturn.mli