cparser: support for attributes over struct and union.

cparser: added experimental emulation of packed structs (PackedStruct.ml)



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

17 files changed, 613 insertions, 135 deletions

diff --git a/cparser/.depend b/cparser/.depend
index d2338ef..2d6b280 100644
--- a/cparser/.depend
+++ b/cparser/.depend
@@ -1,86 +1,88 @@
-AddCasts.cmi: C.cmi
-Bitfields.cmi: C.cmi
-Builtins.cmi: Env.cmi C.cmi
-Ceval.cmi: Env.cmi C.cmi
-Cleanup.cmi: C.cmi
-C.cmi:
-Cprint.cmi: C.cmi
-Cutil.cmi: Env.cmi C.cmi
-Elab.cmi: C.cmi
-Env.cmi: C.cmi
-Errors.cmi:
-GCC.cmi: Builtins.cmi
-Lexer.cmi: Parser.cmi
-Machine.cmi:
-PackedStructs.cmi: C.cmi
-Parse_aux.cmi:
-Parse.cmi: C.cmi
-Parser.cmi: Cabs.cmo
-Rename.cmi: C.cmi
-SimplExpr.cmi: C.cmi
-StructAssign.cmi: C.cmi
-StructByValue.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
-Builtins.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmi
-Cabshelper.cmo: Cabs.cmo
-Cabshelper.cmx: Cabs.cmx
-Cabs.cmo:
-Cabs.cmx:
-Ceval.cmo: Machine.cmi Cutil.cmi C.cmi Ceval.cmi
-Ceval.cmx: Machine.cmx Cutil.cmx C.cmi Ceval.cmi
-Cleanup.cmo: Cutil.cmi C.cmi Cleanup.cmi
-Cleanup.cmx: Cutil.cmx C.cmi Cleanup.cmi
-Cprint.cmo: C.cmi Cprint.cmi
-Cprint.cmx: C.cmi Cprint.cmi
-Cutil.cmo: Machine.cmi Errors.cmi Env.cmi Cprint.cmi C.cmi Cutil.cmi
-Cutil.cmx: Machine.cmx Errors.cmx Env.cmx Cprint.cmx C.cmi Cutil.cmi
+AddCasts.cmi: C.cmi 
+Bitfields.cmi: C.cmi 
+Builtins.cmi: Env.cmi C.cmi 
+C.cmi: 
+Ceval.cmi: Env.cmi C.cmi 
+Cleanup.cmi: C.cmi 
+Cprint.cmi: C.cmi 
+Cutil.cmi: Env.cmi C.cmi 
+Elab.cmi: C.cmi 
+Env.cmi: C.cmi 
+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 
+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 
+Builtins.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmi 
+Cabs.cmo: 
+Cabs.cmx: 
+Cabshelper.cmo: Cabs.cmo 
+Cabshelper.cmx: Cabs.cmx 
+Ceval.cmo: Machine.cmi Cutil.cmi C.cmi Ceval.cmi 
+Ceval.cmx: Machine.cmx Cutil.cmx C.cmi Ceval.cmi 
+Cleanup.cmo: Cutil.cmi C.cmi Cleanup.cmi 
+Cleanup.cmx: Cutil.cmx C.cmi Cleanup.cmi 
+Cprint.cmo: C.cmi Cprint.cmi 
+Cprint.cmx: C.cmi Cprint.cmi 
+Cutil.cmo: Machine.cmi Errors.cmi Env.cmi Cprint.cmi C.cmi Cutil.cmi 
+Cutil.cmx: Machine.cmx Errors.cmx Env.cmx Cprint.cmx C.cmi Cutil.cmi 
 Elab.cmo: Parser.cmi Machine.cmi Lexer.cmi Errors.cmi Env.cmi Cutil.cmi \
     Cprint.cmi Cleanup.cmi Ceval.cmi Cabshelper.cmo Cabs.cmo C.cmi \
-    Builtins.cmi Elab.cmi
+    Builtins.cmi Elab.cmi 
 Elab.cmx: Parser.cmx Machine.cmx Lexer.cmx Errors.cmx Env.cmx Cutil.cmx \
     Cprint.cmx Cleanup.cmx Ceval.cmx Cabshelper.cmx Cabs.cmx C.cmi \
-    Builtins.cmx Elab.cmi
-Env.cmo: C.cmi Env.cmi
-Env.cmx: C.cmi Env.cmi
-Errors.cmo: Errors.cmi
-Errors.cmx: Errors.cmi
-GCC.cmo: Cutil.cmi C.cmi Builtins.cmi GCC.cmi
-GCC.cmx: Cutil.cmx C.cmi Builtins.cmx GCC.cmi
-Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Lexer.cmi
-Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Lexer.cmi
-Machine.cmo: Machine.cmi
-Machine.cmx: Machine.cmi
-Main.cmo: Parse.cmi GCC.cmi Cprint.cmi Builtins.cmi
-Main.cmx: Parse.cmx GCC.cmx Cprint.cmx Builtins.cmx
+    Builtins.cmx Elab.cmi 
+Env.cmo: C.cmi Env.cmi 
+Env.cmx: C.cmi Env.cmi 
+Errors.cmo: Errors.cmi 
+Errors.cmx: Errors.cmi 
+GCC.cmo: Cutil.cmi C.cmi Builtins.cmi GCC.cmi 
+GCC.cmx: Cutil.cmx C.cmi Builtins.cmx GCC.cmi 
+Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Lexer.cmi 
+Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Lexer.cmi 
+Machine.cmo: Machine.cmi 
+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: Errors.cmi Env.cmi Cutil.cmi C.cmi Builtins.cmi \
-    PackedStructs.cmi
+    PackedStructs.cmi 
 PackedStructs.cmx: Errors.cmx Env.cmx Cutil.cmx C.cmi Builtins.cmx \
-    PackedStructs.cmi
-Parse_aux.cmo: Errors.cmi Cabshelper.cmo Parse_aux.cmi
-Parse_aux.cmx: Errors.cmx Cabshelper.cmx Parse_aux.cmi
+    PackedStructs.cmi 
 Parse.cmo: Unblock.cmi StructByValue.cmi StructAssign.cmi SimplExpr.cmi \
-    Rename.cmi Errors.cmi Elab.cmi Bitfields.cmi AddCasts.cmi Parse.cmi
+    Rename.cmi PackedStructs.cmi Errors.cmi Elab.cmi Bitfields.cmi \
+    AddCasts.cmi Parse.cmi 
 Parse.cmx: Unblock.cmx StructByValue.cmx StructAssign.cmx SimplExpr.cmx \
-    Rename.cmx Errors.cmx Elab.cmx Bitfields.cmx AddCasts.cmx Parse.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
+    Rename.cmx PackedStructs.cmx Errors.cmx Elab.cmx Bitfields.cmx \
+    AddCasts.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 
 StructAssign.cmo: Transform.cmi Machine.cmi Errors.cmi Env.cmi Cutil.cmi \
-    C.cmi StructAssign.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
-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
-Unblock.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi Unblock.cmi
+    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 
+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 
+Unblock.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi Unblock.cmi 
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 472b6a4..5ab4eb4 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -116,10 +116,10 @@ let rec transf_members env id count = function
         end
       end
 
-let transf_composite env su id ml =
+let transf_composite env su id attr ml =
   match su with
-  | Struct -> transf_members env id 1 ml
-  | Union  -> ml
+  | Struct -> (attr, transf_members env id 1 ml)
+  | Union  -> (attr, ml)
 
 (* Bitfield manipulation expressions *)
 
diff --git a/cparser/C.mli b/cparser/C.mli
index 9d5a7d7..35e872d 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -231,8 +231,9 @@ type globdecl =
 and globdecl_desc =
   | Gdecl of decl           (* variable declaration, function prototype *)
   | Gfundef of fundef                   (* function definition *)
-  | Gcompositedecl of struct_or_union * ident (* struct/union declaration *)
-  | Gcompositedef of struct_or_union * ident * field list
+  | Gcompositedecl of struct_or_union * ident * attributes
+                                        (* struct/union declaration *)
+  | Gcompositedef of struct_or_union * ident * attributes * field list
                                         (* struct/union definition *)
   | Gtypedef of ident * typ             (* typedef *)
   | Genumdef of ident * (ident * exp option) list  (* enum definition *)
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index be28989..17b2f98 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -143,7 +143,7 @@ let rec add_needed_globdecls accu = function
           if needed f.fd_name
           then (add_fundef f; add_needed_globdecls accu rem)
           else add_needed_globdecls (g :: accu) rem
-      | Gcompositedef(_, id, flds) ->
+      | Gcompositedef(_, id, _, flds) ->
           if needed id
           then (List.iter add_field flds; add_needed_globdecls accu rem)
           else add_needed_globdecls (g :: accu) rem
@@ -176,8 +176,8 @@ let rec simpl_globdecls accu = function
         match g.gdesc with
         | Gdecl((sto, id, ty, init) as decl) -> visible_decl decl || needed id
         | Gfundef f -> f.fd_storage = Storage_default || needed f.fd_name
-        | Gcompositedecl(_, id) -> needed id
-        | Gcompositedef(_, id, flds) -> needed id
+        | Gcompositedecl(_, id, _) -> needed id
+        | Gcompositedef(_, id, _, flds) -> needed id
         | Gtypedef(id, ty) -> needed id
         | Genumdef(id, enu) -> List.exists (fun (id, _) -> needed id) enu
         | Gpragma s -> true in
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 3d023a8..5887e87 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -470,13 +470,15 @@ let globdecl pp g =
       fprintf pp "%a@ @ " full_decl d
   | Gfundef f ->
       fundef pp f
-  | Gcompositedecl(kind, id) ->
-      fprintf pp "%s %a;@ @ "
+  | Gcompositedecl(kind, id, attrs) ->
+      fprintf pp "%s%a %a;@ @ "
         (match kind with Struct -> "struct" | Union -> "union")
+        attributes attrs
         ident id
-  | Gcompositedef(kind, id, flds) ->
-      fprintf pp "@[<v 2>%s %a {"
+  | Gcompositedef(kind, id, attrs, flds) ->
+      fprintf pp "@[<v 2>%s%a %a {"
         (match kind with Struct -> "struct" | Union -> "union")
+        attributes attrs
         ident id;
       List.iter (fun fld -> fprintf pp "@ %a;" field fld) flds;
       fprintf pp "@;<0 -2>};@]@ @ "
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 7aac659..2e664df 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -107,8 +107,10 @@ let rec attributes_of_type env t =
   | TArray(ty, sz, a) -> add_attributes a (attributes_of_type env ty)
   | TFun(ty, params, vararg, a) -> a
   | TNamed(s, a) -> attributes_of_type env (unroll env t)
-  | TStruct(s, a) -> a
-  | TUnion(s, a) -> a
+  | TStruct(s, a) -> 
+      let ci = Env.find_struct env s in add_attributes ci.ci_attr a
+  | TUnion(s, a) ->
+      let ci = Env.find_union env s in add_attributes ci.ci_attr a
 
 (* Changing the attributes of a type (at top-level) *)
 (* Same hack as above for array types. *)
@@ -377,16 +379,20 @@ let incomplete_type env t =
 
 (* Computing composite_info records *)
 
-let composite_info_decl env su =
-  { ci_kind = su; ci_members = []; ci_alignof = None; ci_sizeof = None }
+let composite_info_decl env su attr =
+  { ci_kind = su; ci_members = [];
+    ci_alignof = None; ci_sizeof = None;
+    ci_attr = attr }
 
-let composite_info_def env su m =
+let composite_info_def env su attr m =
   { ci_kind = su; ci_members = m;
     ci_alignof = alignof_struct_union env m;
     ci_sizeof =
-      match su with
+      begin match su with
       | Struct -> sizeof_struct env m
-      | Union -> sizeof_union env m }
+      | Union -> sizeof_union env m
+      end;
+    ci_attr = attr }
 
 (* Type of a function definition *)
 
@@ -646,6 +652,17 @@ let is_literal_0 e =
   | EConst(CInt(0L, _, _)) -> true
   | _ -> false
 
+(* Assignment compatibility check over attributes.
+   Standard attributes ("const", "volatile", "restrict") can safely
+   be added (to the rhs type to get the lhs type) but must not be dropped.
+   Custom attributes can safely be dropped but must not be added. *)
+
+let valid_assignment_attr afrom ato =
+  let is_covariant = function Attr _ -> false | _ -> true in
+  let (afrom1, afrom2) = List.partition is_covariant afrom
+  and (ato1, ato2) = List.partition is_covariant ato in
+  incl_attributes afrom1 ato1 && incl_attributes ato2 afrom2
+
 (* Check that an assignment is allowed *)
 
 let valid_assignment env from tto =
@@ -653,7 +670,8 @@ let valid_assignment env from tto =
   | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true
   | TInt _, TPtr _ -> is_literal_0 from
   | TPtr(ty, _), TPtr(ty', _) ->
-      incl_attributes (attributes_of_type env ty) (attributes_of_type env ty')
+      valid_assignment_attr (attributes_of_type env ty)
+                            (attributes_of_type env ty')
       && (is_void_type env ty || is_void_type env ty'
           || compatible_types env
                (erase_attributes_type env ty)
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index d4c9441..7bd9119 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -69,8 +69,10 @@ val incomplete_type : Env.t -> typ -> bool
 
 (* Computing composite_info records *)
 
-val composite_info_decl: Env.t -> struct_or_union -> Env.composite_info
-val composite_info_def: Env.t -> struct_or_union -> field list -> Env.composite_info
+val composite_info_decl:
+  Env.t -> struct_or_union -> attributes -> Env.composite_info
+val composite_info_def:
+  Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info
 
 (* Type classification functions *)
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index bbb049e..eaba8d8 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -417,15 +417,13 @@ let rec elab_specifier ?(only = false) loc env specifier =
 
     | [Cabs.Tstruct(id, optmembers, a)] ->
         let (id', env') =
-          elab_struct_or_union only Struct loc id optmembers env in
-        let attr' = add_attributes !attr (elab_attributes loc env a) in
-        (!sto, !inline, TStruct(id', attr'), env')
+          elab_struct_or_union only Struct loc id optmembers a env in
+        (!sto, !inline, TStruct(id', !attr), env')
 
     | [Cabs.Tunion(id, optmembers, a)] ->
         let (id', env') =
-          elab_struct_or_union only Union loc id optmembers env in
-        let attr' = add_attributes !attr (elab_attributes loc env a) in
-        (!sto, !inline, TUnion(id', attr'), env')
+          elab_struct_or_union only Union loc id optmembers a env in
+        (!sto, !inline, TUnion(id', !attr), env')
 
     | [Cabs.Tenum(id, optmembers, a)] ->
         let env' = 
@@ -581,7 +579,7 @@ and elab_field_group env (spec, fieldlist) =
 
 (* Elaboration of a struct or union *)
 
-and elab_struct_or_union_info kind loc env members =
+and elab_struct_or_union_info kind loc env members attrs =
   let (m, env') = mmap elab_field_group env members in
   let m = List.flatten m in
   (* Check for incomplete types *)
@@ -594,11 +592,16 @@ and elab_struct_or_union_info kind loc env members =
         error loc "member '%s' has incomplete type" fld.fld_name;
       check_incomplete rem in
   check_incomplete m;
-  (composite_info_def env' kind m, env')
+  (composite_info_def env' kind attrs m, env')
 
 (* Elaboration of a struct or union *)
 
-and elab_struct_or_union only kind loc tag optmembers env =
+and elab_struct_or_union only kind loc tag optmembers attrs env =
+  let attrs' =
+    elab_attributes loc env attrs in
+  let warn_attrs () =
+    if attrs' <> [] then
+      warning loc "attributes over struct/union ignored in this context" in
   let optbinding =
     if tag = "" then None else Env.lookup_composite env tag in
   match optbinding, optmembers with
@@ -609,16 +612,17 @@ and elab_struct_or_union only kind loc tag optmembers env =
          and the composite was bound in another scope,
          create a new incomplete composite instead via the case
          "_, None" below. *)
+      warn_attrs();
       (tag', env)
   | Some(tag', ({ci_sizeof = None} as ci)), Some members
     when Env.in_current_scope env tag' ->
       if ci.ci_kind <> kind then
         error loc "struct/union mismatch on tag '%s'" tag;
       (* finishing the definition of an incomplete struct or union *)
-      let (ci', env') = elab_struct_or_union_info kind loc env members in
+      let (ci', env') = elab_struct_or_union_info kind loc env members attrs' in
       (* Emit a global definition for it *)
       emit_elab (elab_loc loc)
-                (Gcompositedef(kind, tag', ci'.ci_members));
+                (Gcompositedef(kind, tag', attrs', ci'.ci_members));
       (* Replace infos but keep same ident *)
       (tag', Env.add_composite env' tag' ci')
   | Some(tag', {ci_sizeof = Some _}), Some _
@@ -629,26 +633,27 @@ and elab_struct_or_union only kind loc tag optmembers env =
       (* declaration of an incomplete struct or union *)
       if tag = "" then
         error loc "anonymous, incomplete struct or union";
-      let ci = composite_info_decl env kind in
+      let ci = composite_info_decl env kind attrs' in
       (* enter it with a new name *)
       let (tag', env') = Env.enter_composite env tag ci in
       (* emit it *)
       emit_elab (elab_loc loc)
-                (Gcompositedecl(kind, tag'));
+                (Gcompositedecl(kind, tag', attrs'));
       (tag', env')
   | _, Some members ->
       (* definition of a complete struct or union *)
-      let ci1 = composite_info_decl env kind in
+      let ci1 = composite_info_decl env kind attrs' in
       (* enter it, incomplete, with a new name *)
       let (tag', env') = Env.enter_composite env tag ci1 in
       (* emit a declaration so that inner structs and unions can refer to it *)
       emit_elab (elab_loc loc)
-                (Gcompositedecl(kind, tag'));
+                (Gcompositedecl(kind, tag', attrs'));
       (* elaborate the members *)
-      let (ci2, env'') = elab_struct_or_union_info kind loc env' members in
+      let (ci2, env'') =
+        elab_struct_or_union_info kind loc env' members attrs' in
       (* emit a definition *)
       emit_elab (elab_loc loc)
-                (Gcompositedef(kind, tag', ci2.ci_members));
+                (Gcompositedef(kind, tag', attrs', ci2.ci_members));
       (* Replace infos but keep same ident *)
       (tag', Env.add_composite env'' tag' ci2)
 
diff --git a/cparser/Env.ml b/cparser/Env.ml
index 777b3e1..164fe59 100644
--- a/cparser/Env.ml
+++ b/cparser/Env.ml
@@ -65,6 +65,7 @@ type composite_info = {
   ci_members: field list;               (* members, in order *)
   ci_alignof: int option;               (* alignment; None if incomplete *)
   ci_sizeof: int option;                (* size; None if incomplete *)
+  ci_attr: attributes                   (* attributes, if any *)
 }
 
 (* Infos associated with an ordinary identifier *)
diff --git a/cparser/Env.mli b/cparser/Env.mli
index e7a74af..01f95ca 100644
--- a/cparser/Env.mli
+++ b/cparser/Env.mli
@@ -29,6 +29,7 @@ type composite_info = {
   ci_members: C.field list;             (* members, in order *)
   ci_alignof: int option;               (* alignment; None if incomplete *)
   ci_sizeof: int option;                (* size; None if incomplete *)
+  ci_attr: C.attributes                 (* attributes, if any *)
 }
 
 type ident_info = II_ident of C.storage * C.typ | II_enum of int64
diff --git a/cparser/Makefile b/cparser/Makefile
index f4c1274..9767b48 100644
--- a/cparser/Makefile
+++ b/cparser/Makefile
@@ -16,7 +16,7 @@ SRCS=Errors.ml Cabs.ml Cabshelper.ml Parse_aux.ml Parser.ml Lexer.ml \
   Cleanup.ml Elab.ml Rename.ml \
   Transform.ml \
   Unblock.ml SimplExpr.ml AddCasts.ml StructByValue.ml StructAssign.ml \
-  Bitfields.ml \
+  Bitfields.ml PackedStructs.ml \
   Parse.ml
 
 COBJS=uint64.o
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
new file mode 100644
index 0000000..edd45ff
--- /dev/null
+++ b/cparser/PackedStructs.ml
@@ -0,0 +1,434 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Emulation of #pragma pack (experimental) *)
+
+open Printf
+open C
+open Cutil
+open Env
+open Errors
+
+type field_info = {
+  fi_offset: int;                       (* byte offset within struct *)
+  fi_swap: ikind option                 (* Some ik if byte-swapped *)
+}
+
+(* Mapping from (struct name, field name) to field_info.
+   Only fields of packed structs are mentioned in this table. *)
+
+let packed_fields : (ident * string, field_info) Hashtbl.t
+                  = Hashtbl.create 57
+
+(* The current packing parameters.  The first two are 0 if packing is
+   turned off. *)
+
+let max_field_align = ref 0
+let min_struct_align = ref 0
+let byte_swap_fields = ref false
+
+(* Alignment *)
+
+let is_pow2 n =
+  n > 0 && n land (n - 1) == 0
+
+let align x boundary =
+  assert (is_pow2 boundary);
+  (x + boundary - 1) land (lnot (boundary - 1))
+
+(* Layout algorithm *)
+
+let layout_struct mfa msa swapped loc env struct_id fields =
+  let rec layout max_al pos = function
+  | [] ->
+      (max_al, pos)
+  | f :: rem -> 
+      if f.fld_bitfield <> None then
+        error "%a: Error: bitfields in packed structs not allowed"
+              formatloc loc;
+      let swap =
+        if swapped then begin
+          match unroll env f.fld_typ with
+          | TInt(ik, _) ->
+              if sizeof_ikind ik = 1 then None else Some ik
+          | _ ->
+              error "%a: Error: byte-swapped fields must have integer type"
+                    formatloc loc;
+              None
+        end else
+          None in
+      let (sz, al) =
+        match sizeof env f.fld_typ, alignof env f.fld_typ with
+        | Some s, Some a -> (s, a)
+        | _, _ -> error "%a: struct field has incomplete type" formatloc loc;
+                  (0, 1) in
+      let al1 = min al mfa in
+      let pos1 = align pos al1 in
+      Hashtbl.add packed_fields
+         (struct_id, f.fld_name)
+         {fi_offset = pos1; fi_swap = swap};
+      let pos2 = pos1 + sz in
+      layout (max max_al al1) pos2 rem in
+  let (al, sz) = layout 1 0 fields in
+  if al >= msa then
+    (0, sz)
+  else
+    (msa, align sz msa)
+
+(* Rewriting of struct declarations *)
+
+let transf_composite loc env su id attrs ml =
+  match su with
+  | Union -> (attrs, ml)
+  | Struct ->
+      let (mfa, msa, swapped) =
+        if !max_field_align > 0 then
+          (!max_field_align, !min_struct_align, !byte_swap_fields)
+        else if find_custom_attributes ["packed";"__packed__"] attrs <> [] then
+          (1, 0, false)
+        else
+          (0, 0, false) in
+      if mfa = 0 then (attrs, ml) else begin
+        let (al, sz) = layout_struct mfa msa swapped loc env id ml in
+        let attrs =
+          if al = 0 then attrs else
+            add_attributes [Attr("__aligned__", [AInt(Int64.of_int al)])] attrs
+        and field =
+          {fld_name = "__payload";
+           fld_typ = TArray(TInt(IChar, []), Some(Int64.of_int sz), []);
+           fld_bitfield = None}
+        in (attrs, [field])
+      end
+
+(* Accessor functions *)
+
+let lookup_function loc env name =
+  try
+    match Env.lookup_ident env name with
+    | (id, II_ident(sto, ty)) -> (id, ty)
+    | (id, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name))
+  with Env.Error msg ->
+    fatal_error "%a: Error: %s" formatloc loc (Env.error_message msg)
+
+(*  (ty) e *)
+let ecast ty e = {edesc = ECast(ty, e); etyp = ty}
+
+(*  *e  *)
+let ederef ty e = {edesc = EUnop(Oderef, e); etyp = ty}
+
+(*  e + n *)
+let eoffset e n =
+  {edesc = EBinop(Oadd, e, intconst (Int64.of_int n) IInt, e.etyp);
+   etyp = e.etyp}
+
+(*  *((ty * ) (base.__payload + offset))  *)
+let dot_packed_field base pf ty =
+  let payload =
+    {edesc = EUnop(Odot "__payload", base);
+     etyp = TArray(TInt(IChar,[]),None,[]) } in
+  ederef ty (ecast (TPtr(ty, [])) (eoffset payload pf.fi_offset))
+
+(*  *((ty * ) (base->__payload + offset))  *)
+let arrow_packed_field base pf ty =
+  let payload =
+    {edesc = EUnop(Oarrow "__payload", base);
+     etyp = TArray(TInt(IChar,[]),None,[]) } in
+  ederef ty (ecast (TPtr(ty, [])) (eoffset payload pf.fi_offset))
+
+(*  (ty) __builtin_read_intNN_reversed(&lval)  *)
+let bswap_read loc env lval ik =
+  let uik = unsigned_ikind_of ik in
+  let bsize = sizeof_ikind ik * 8 in
+  let (id, fty) =
+    lookup_function loc env (sprintf "__builtin_read_int%d_reversed" bsize) in
+  let fn = {edesc = EVar id; etyp = fty} in
+  let args =
+    if uik = ik
+    then [eaddrof lval]
+    else [ecast (TPtr(TInt(uik,[]),[])) (eaddrof lval)] in
+  let call = {edesc = ECall(fn, args); etyp = TInt(uik, [])} in
+  if ik = uik then call else ecast (TInt(ik,[])) call
+
+(*  __builtin_write_intNN_reversed(&lhs,rhs)  *)
+let bswap_write loc env lhs rhs ik =
+  let uik = unsigned_ikind_of ik in
+  let bsize = sizeof_ikind ik * 8 in
+  let (id, fty) =
+    lookup_function loc env (sprintf "__builtin_write_int%d_reversed" bsize) in
+  let fn = {edesc = EVar id; etyp = fty} in
+  let args =
+    if uik = ik
+    then [eaddrof lhs; rhs]
+    else [ecast (TPtr(TInt(uik,[]),[])) (eaddrof lhs);
+          ecast (TInt(uik,[])) rhs] in
+  {edesc = ECall(fn, args); etyp = TVoid[]}
+
+(* Expressions *)
+
+type context = Val | Effects
+
+let transf_expr loc env ctx e =
+
+  let is_packed_access ty fieldname =
+    match unroll env ty with
+    | TStruct(id, _) ->
+        (try Some(Hashtbl.find packed_fields (id, fieldname))
+         with Not_found -> None)
+    | _ -> None in
+
+  let is_packed_access_ptr ty fieldname =
+    match unroll env ty with
+    | TPtr(ty', _) -> is_packed_access ty' fieldname
+    | _ -> None in 
+
+  (* Transformation of l-values.  Return transformed expr plus
+     [Some ik] if l-value is a byte-swapped field of kind [ik]
+     or [None] otherwise. *)
+  let rec lvalue e =
+    match e.edesc with
+    | EUnop(Odot fieldname, e1) ->
+        let e1' = texp Val e1 in
+        begin match is_packed_access e1.etyp fieldname with
+        | None ->
+            ({edesc = EUnop(Odot fieldname, e1'); etyp = e.etyp}, None)
+        | Some pf ->
+            (dot_packed_field e1' pf e.etyp, pf.fi_swap)
+        end
+    | EUnop(Oarrow fieldname, e1) ->
+        let e1' = texp Val e1 in
+        begin match is_packed_access_ptr e1.etyp fieldname with
+        | None ->
+            ({edesc = EUnop(Oarrow fieldname, e1'); etyp = e.etyp}, None)
+        | Some pf ->
+            (arrow_packed_field e1' pf e.etyp, pf.fi_swap)
+        end
+    | _ ->
+        (texp Val e, None) 
+
+  and texp ctx e =
+    match e.edesc with
+    | EConst _ -> e
+    | ESizeof _ -> e
+    | EVar _ -> e
+
+    | EUnop(Odot _, _) | EUnop(Oarrow _, _) ->
+        let (e', swap) = lvalue e in
+        begin match swap with
+        | None -> e'
+        | Some ik -> bswap_read loc env e' ik
+        end
+
+    | EUnop((Oaddrof|Opreincr|Opredecr|Opostincr|Opostdecr as op), e1) ->
+        let (e1', swap) = lvalue e1 in
+        if swap <> None then
+          error "%a: Error: &, ++ and -- over byte-swap field are not supported"
+                formatloc loc;
+        {edesc = EUnop(op, e1'); etyp = e.etyp}
+
+    | EUnop(op, e1) ->
+        {edesc = EUnop(op, texp Val e1); etyp = e.etyp}
+
+    | EBinop(Oassign, e1, e2, ty) ->
+        let (e1', swap) = lvalue e1 in
+        let e2' = texp Val e2 in
+        begin match swap with
+        | None ->
+            {edesc = EBinop(Oassign, e1', e2', ty); etyp = e.etyp}
+        | Some ik ->
+            if ctx <> Effects then
+              error "%a: Error: assignment over byte-swapped field in value context is not supported"
+                    formatloc loc;
+            bswap_write loc env e1' e2' ik
+        end
+
+    | 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) ->
+        let (e1', swap) = lvalue e1 in
+        let e2' = texp Val e2 in
+        if swap <> None then
+          error "%a: Error: op-assignment over byte-swapped field in value context is not supported"
+                formatloc loc;
+        {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp}
+
+    | EBinop(Ocomma, e1, e2, ty) ->
+        {edesc = EBinop(Ocomma, texp Effects e1, texp Val 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 rec transf_stmt env s =
+  match s.sdesc with
+  | Sskip -> s
+  | Sdo e ->
+      {sdesc = Sdo(transf_expr s.sloc env Effects e); sloc = s.sloc}
+  | Sseq(s1, s2) -> 
+      {sdesc = Sseq(transf_stmt env s1, transf_stmt env s2); sloc = s.sloc }
+  | Sif(e, s1, s2) ->
+      {sdesc = Sif(transf_expr s.sloc env Val e,
+                   transf_stmt env s1, transf_stmt env s2);
+       sloc = s.sloc}
+  | Swhile(e, s1) ->
+      {sdesc = Swhile(transf_expr s.sloc env Val e, transf_stmt env s1);
+       sloc = s.sloc}
+  | Sdowhile(s1, e) ->
+      {sdesc = Sdowhile(transf_stmt env s1, transf_expr s.sloc env Val e);
+       sloc = s.sloc}
+  | Sfor(s1, e, s2, s3) ->
+      {sdesc = Sfor(transf_stmt env s1, transf_expr s.sloc env Val e,
+                    transf_stmt env s2, transf_stmt env s3);
+       sloc = s.sloc}
+  | Sbreak -> s
+  | Scontinue -> s
+  | Sswitch(e, s1) ->
+      {sdesc = Sswitch(transf_expr s.sloc env Val e,
+                       transf_stmt env s1); sloc = s.sloc}
+  | Slabeled(lbl, s) ->
+      {sdesc = Slabeled(lbl, transf_stmt env s); sloc = s.sloc}
+  | Sgoto lbl -> s
+  | Sreturn None -> s
+  | Sreturn (Some e) ->
+      {sdesc = Sreturn(Some(transf_expr s.sloc env Val e)); sloc = s.sloc}
+  | Sblock _ | Sdecl _ ->
+      assert false     (* should not occur in unblocked code *)
+
+(* Functions *)
+
+let transf_fundef env f =
+  { f with fd_body = transf_stmt env f.fd_body }
+
+(* Initializers *)
+
+let rec check_init i =
+  match i with
+  | Init_single e -> true
+  | Init_array il -> List.for_all check_init il
+  | Init_struct(id, fld_init_list) ->
+      List.for_all
+        (fun (f, i) ->
+          not (Hashtbl.mem packed_fields (id, f.fld_name)))
+        fld_init_list
+  | Init_union(id, fld, i) ->
+      check_init i
+
+(* Declarations *)
+
+let transf_decl loc env (sto, id, ty, init_opt as decl) =
+  begin match init_opt with
+  | None -> () 
+  | Some i ->
+      if not (check_init i) then
+        error "%a: Error: Initialization of packed structs is not supported"
+              formatloc loc
+  end;
+  decl
+
+(* Pragmas *)
+
+let re_pack = Str.regexp "pack\\b"
+let re_pack_1 = Str.regexp "pack[ \t]*(\\([ \t0-9,]*\\))[ \t]*$"
+let re_comma = Str.regexp ",[ \t]*"
+
+let process_pragma loc s =
+  if Str.string_match re_pack s 0 then begin
+    if Str.string_match re_pack_1 s 0 then begin
+      let arg = Str.matched_group 1 s in
+      let (mfa, msa, bs) =
+        match List.map int_of_string (Str.split re_comma arg) with
+        | [] -> (0, 0, false)
+        | [x] -> (x, 0, false)
+        | [x;y] -> (x, y, false)
+        | x :: y :: z :: _ -> (x, y, z = 1) in
+      if mfa = 0 || is_pow2 mfa then
+        max_field_align := mfa
+      else
+        error "%a: Error: In #pragma pack, max field alignment must be a power of 2" formatloc loc;
+      if msa = 0 || is_pow2 msa then
+        min_struct_align := msa
+      else
+        error "%a: Error: In #pragma pack, min struct alignment must be a power of 2" formatloc loc;
+      byte_swap_fields := bs;
+      true
+    end else begin
+      warning "%a: Warning: Ill-formed #pragma pack, ignored" formatloc loc;
+      false
+    end
+  end else
+    false
+
+(* Global declarations *)
+
+let rec transf_globdecls env accu = function
+  | [] -> List.rev accu
+  | g :: gl ->
+      match g.gdesc with
+      | Gdecl((sto, id, ty, init) as d) ->
+          transf_globdecls
+            (Env.add_ident env id sto ty)
+            ({g with gdesc = Gdecl(transf_decl g.gloc env d)} :: accu)
+            gl
+      | Gfundef f ->
+          transf_globdecls
+            (Env.add_ident env f.fd_name f.fd_storage (fundef_typ f))
+            ({g with gdesc = Gfundef(transf_fundef env f)} :: accu)
+            gl
+      | Gcompositedecl(su, id, attr) ->
+          transf_globdecls
+            (Env.add_composite env id (composite_info_decl env su attr))
+            (g :: accu)
+            gl
+      | Gcompositedef(su, id, attr, fl) ->
+          let (attr', fl') = transf_composite g.gloc env su id attr fl in
+          transf_globdecls
+            (Env.add_composite env id (composite_info_def env su attr' fl'))
+            ({g with gdesc = Gcompositedef(su, id, attr', fl')} :: accu)
+            gl
+      | Gtypedef(id, ty) ->
+          transf_globdecls
+            (Env.add_typedef env id ty)
+            (g :: accu)
+            gl
+      | Genumdef _  ->
+          transf_globdecls
+            env
+            (g :: accu)
+            gl
+      | Gpragma p ->
+          if process_pragma g.gloc p
+          then transf_globdecls env accu gl
+          else transf_globdecls env (g :: accu) gl
+
+(* Program *)
+
+let program p =
+  min_struct_align := 0;
+  max_field_align := 0;
+  byte_swap_fields := false;
+  transf_globdecls (Builtins.environment()) [] p
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index ed988f9..abef83c 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -24,9 +24,10 @@ let transform_program t p =
   (run_pass (SimplExpr.program ~volatile:(CharSet.mem 'v' t)) 'e'
   (run_pass StructAssign.program 'S'
   (run_pass StructByValue.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
@@ -40,6 +41,7 @@ let parse_transformations s =
             | 'S' -> set "bsS"
             | 'v' -> set "ev"
             | 'f' -> set "bf"
+            | 'p' -> set "bp"
             |  _  -> ())
     s;
   !t
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index 4b2f350..d58c8ad 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -197,11 +197,12 @@ and globdecl_desc env = function
   | Gfundef fd ->
       let (fd', env') = fundef env fd in
       (Gfundef fd', env')
-  | Gcompositedecl(kind, id) ->
+  | Gcompositedecl(kind, id, attr) ->
       let (id', env') = rename env id in
-      (Gcompositedecl(kind, id'), env')
-  | Gcompositedef(kind, id, members) ->
-      (Gcompositedef(kind, ident env id, List.map (field env) members), env)
+      (Gcompositedecl(kind, id', attr), env')
+  | Gcompositedef(kind, id, attr, members) ->
+      (Gcompositedef(kind, ident env id, attr, List.map (field env) members),
+       env)
   | Gtypedef(id, ty) ->
       let (id', env') = rename env id in
       (Gtypedef(id', typ env' ty), env')
diff --git a/cparser/StructByValue.ml b/cparser/StructByValue.ml
index c66af32..60c1154 100644
--- a/cparser/StructByValue.ml
+++ b/cparser/StructByValue.ml
@@ -22,7 +22,7 @@ open C
 open Cutil
 open Transform
 
-(* In function argument types, struct s -> struct s *
+(* In function argument types, struct s -> const struct s *
    In function result types, struct s -> void + add 1st parameter struct s *
    Try to preserve original typedef names when no change.
 *)
@@ -286,8 +286,8 @@ let transf_fundef env f =
 
 (* Composites *)
 
-let transf_composite env su id fl =
-  List.map (fun f -> {f with fld_typ = transf_type env f.fld_typ}) fl
+let transf_composite env su id attr fl =
+  (attr, List.map (fun f -> {f with fld_typ = transf_type env f.fld_typ}) fl)
 
 (* Entry point *)
 
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index 911d613..4fd83ae 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -45,8 +45,10 @@ let get_temps () =
 let program
     ?(decl = fun env d -> d)
     ?(fundef = fun env fd -> fd)
-    ?(composite = fun env su id fl -> fl)
+    ?(composite = fun env su id attr fl -> (attr, fl))
     ?(typedef = fun env id ty -> ty)
+    ?(enum = fun env id members -> members)
+    ?(pragma = fun env s -> s)
     p =
 
   let rec transf_globdecls env accu = function
@@ -59,16 +61,19 @@ let program
         | Gfundef f ->
            (Gfundef(fundef env f),
             Env.add_ident env f.fd_name f.fd_storage (fundef_typ f))
-        | Gcompositedecl(su, id) ->
-            (Gcompositedecl(su, id),
-             Env.add_composite env id (composite_info_decl env su))
-        | Gcompositedef(su, id, fl) ->
-            (Gcompositedef(su, id, composite env su id fl),
-             Env.add_composite env id (composite_info_def env su fl))
+        | Gcompositedecl(su, id, attr) ->
+            (Gcompositedecl(su, id, attr),
+             Env.add_composite env id (composite_info_decl env su attr))
+        | Gcompositedef(su, id, attr, fl) ->
+            let (attr', fl') = composite env su id attr fl in
+            (Gcompositedef(su, id, attr', fl'),
+             Env.add_composite env id (composite_info_def env su attr fl))
         | Gtypedef(id, ty) ->
             (Gtypedef(id, typedef env id ty), Env.add_typedef env id ty)
-        | Genumdef _ as gd -> (gd, env)
-        | Gpragma _ as gd -> (gd, env)
+        | Genumdef(id, members) ->
+            (Genumdef(id, enum env id members), env)
+        | Gpragma s ->
+            (Gpragma(pragma env s), env)
       in
         transf_globdecls env' ({g with gdesc = desc'} :: accu) gl
 
diff --git a/cparser/Transform.mli b/cparser/Transform.mli
index 960d890..8f2c5f8 100644
--- a/cparser/Transform.mli
+++ b/cparser/Transform.mli
@@ -23,8 +23,12 @@ val get_temps : unit -> C.decl list
 val program :
   ?decl:(Env.t -> C.decl -> C.decl) ->
   ?fundef:(Env.t -> C.fundef -> C.fundef) ->
-  ?composite:(Env.t ->
-              C.struct_or_union -> C.ident -> C.field list -> C.field list) ->
+  ?composite:(Env.t -> C.struct_or_union -> 
+                C.ident -> C.attributes -> C.field list -> 
+                  C.attributes * C.field list) ->
   ?typedef:(Env.t -> C.ident -> Env.typedef_info -> Env.typedef_info) ->
+  ?enum:(Env.t -> C.ident -> (C.ident * C.exp option) list ->
+                                       (C.ident * C.exp option) list) ->
+  ?pragma:(Env.t -> string -> string) ->
   C.program ->
   C.program