Add support to clightgen for generating Csyntax AST as .v files

As proposed in #404.

This is presented as a new option `-clight` to the existing `clightgen` tool.

Revise clightgen testing to test the Csyntax output in addition to
the Clight output.

8 files changed, 588 insertions, 255 deletions

diff --git a/export/Clightdefs.v b/export/Clightdefs.v
index 708be1cb..dc4e3491 100644
--- a/export/Clightdefs.v
+++ b/export/Clightdefs.v
@@ -14,50 +14,11 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** All imports and definitions used by .v Clight files generated by clightgen *)
+(** Definitions used by .v files generated by clightgen *)
 
-From Coq Require Import Ascii String List ZArith.
-From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight.
-
-(** ** Short names for types *)
-
-Definition tvoid := Tvoid.
-Definition tschar := Tint I8 Signed noattr.
-Definition tuchar := Tint I8 Unsigned noattr.
-Definition tshort := Tint I16 Signed noattr.
-Definition tushort := Tint I16 Unsigned noattr.
-Definition tint := Tint I32 Signed noattr.
-Definition tuint := Tint I32 Unsigned noattr.
-Definition tbool := Tint IBool Unsigned noattr.
-Definition tlong := Tlong Signed noattr.
-Definition tulong := Tlong Unsigned noattr.
-Definition tfloat := Tfloat F32 noattr.
-Definition tdouble := Tfloat F64 noattr.
-Definition tptr (t: type) := Tpointer t noattr.
-Definition tarray (t: type) (sz: Z) := Tarray t sz noattr.
-
-Definition volatile_attr := {| attr_volatile := true; attr_alignas := None |}.
-
-Definition tattr (a: attr) (ty: type) :=
-  match ty with
-  | Tvoid => Tvoid
-  | Tint sz si _ => Tint sz si a
-  | Tlong si _ => Tlong si a
-  | Tfloat sz _ => Tfloat sz a
-  | Tpointer elt _ => Tpointer elt a
-  | Tarray elt sz _ => Tarray elt sz a
-  | Tfunction args res cc => Tfunction args res cc
-  | Tstruct id _ => Tstruct id a
-  | Tunion id  _ => Tunion id a
-  end.
-
-Definition tvolatile (ty: type) := tattr volatile_attr ty.
-
-Definition talignas (n: N) (ty: type) :=
-  tattr {| attr_volatile := false; attr_alignas := Some n |} ty.
-
-Definition tvolatile_alignas (n: N) (ty: type) :=
-  tattr {| attr_volatile := true; attr_alignas := Some n |} ty.
+From Coq Require Import List.
+From compcert Require Import Maps Errors AST Ctypes Clight.
+From compcert Require Export Ctypesdefs.
 
 (** ** Constructor for programs and compilation units *)
 
@@ -86,206 +47,6 @@ Definition mkprogram (types: list composite_definition)
      prog_comp_env := ce;
      prog_comp_env_eq := EQ |}.
 
-(** ** Encoding character strings as positive numbers *)
-
-(** The following encoding of character strings as positive numbers
-    must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *)
-
-Definition append_bit_pos (b: bool) (p: positive) : positive :=
-  if b then xI p else xO p.
-
-Definition append_char_pos_default (c: ascii) (p: positive) : positive :=
-  let '(Ascii b7 b6 b5 b4 b3 b2 b1 b0) := c in
-  xI (xI (xI (xI (xI (xI
-    (append_bit_pos b0 (append_bit_pos b1
-    (append_bit_pos b2 (append_bit_pos b3
-    (append_bit_pos b4 (append_bit_pos b5
-    (append_bit_pos b6 (append_bit_pos b7 p))))))))))))).
-
-Definition append_char_pos (c: ascii) (p: positive) : positive :=
-  match c with
-  | "0"%char => xO (xO (xO (xO (xO (xO p)))))
-  | "1"%char => xI (xO (xO (xO (xO (xO p)))))
-  | "2"%char => xO (xI (xO (xO (xO (xO p)))))
-  | "3"%char => xI (xI (xO (xO (xO (xO p)))))
-  | "4"%char => xO (xO (xI (xO (xO (xO p)))))
-  | "5"%char => xI (xO (xI (xO (xO (xO p)))))
-  | "6"%char => xO (xI (xI (xO (xO (xO p)))))
-  | "7"%char => xI (xI (xI (xO (xO (xO p)))))
-  | "8"%char => xO (xO (xO (xI (xO (xO p)))))
-  | "9"%char => xI (xO (xO (xI (xO (xO p)))))
-  | "a"%char => xO (xI (xO (xI (xO (xO p)))))
-  | "b"%char => xI (xI (xO (xI (xO (xO p)))))
-  | "c"%char => xO (xO (xI (xI (xO (xO p)))))
-  | "d"%char => xI (xO (xI (xI (xO (xO p)))))
-  | "e"%char => xO (xI (xI (xI (xO (xO p)))))
-  | "f"%char => xI (xI (xI (xI (xO (xO p)))))
-  | "g"%char => xO (xO (xO (xO (xI (xO p)))))
-  | "h"%char => xI (xO (xO (xO (xI (xO p)))))
-  | "i"%char => xO (xI (xO (xO (xI (xO p)))))
-  | "j"%char => xI (xI (xO (xO (xI (xO p)))))
-  | "k"%char => xO (xO (xI (xO (xI (xO p)))))
-  | "l"%char => xI (xO (xI (xO (xI (xO p)))))
-  | "m"%char => xO (xI (xI (xO (xI (xO p)))))
-  | "n"%char => xI (xI (xI (xO (xI (xO p)))))
-  | "o"%char => xO (xO (xO (xI (xI (xO p)))))
-  | "p"%char => xI (xO (xO (xI (xI (xO p)))))
-  | "q"%char => xO (xI (xO (xI (xI (xO p)))))
-  | "r"%char => xI (xI (xO (xI (xI (xO p)))))
-  | "s"%char => xO (xO (xI (xI (xI (xO p)))))
-  | "t"%char => xI (xO (xI (xI (xI (xO p)))))
-  | "u"%char => xO (xI (xI (xI (xI (xO p)))))
-  | "v"%char => xI (xI (xI (xI (xI (xO p)))))
-  | "w"%char => xO (xO (xO (xO (xO (xI p)))))
-  | "x"%char => xI (xO (xO (xO (xO (xI p)))))
-  | "y"%char => xO (xI (xO (xO (xO (xI p)))))
-  | "z"%char => xI (xI (xO (xO (xO (xI p)))))
-  | "A"%char => xO (xO (xI (xO (xO (xI p)))))
-  | "B"%char => xI (xO (xI (xO (xO (xI p)))))
-  | "C"%char => xO (xI (xI (xO (xO (xI p)))))
-  | "D"%char => xI (xI (xI (xO (xO (xI p)))))
-  | "E"%char => xO (xO (xO (xI (xO (xI p)))))
-  | "F"%char => xI (xO (xO (xI (xO (xI p)))))
-  | "G"%char => xO (xI (xO (xI (xO (xI p)))))
-  | "H"%char => xI (xI (xO (xI (xO (xI p)))))
-  | "I"%char => xO (xO (xI (xI (xO (xI p)))))
-  | "J"%char => xI (xO (xI (xI (xO (xI p)))))
-  | "K"%char => xO (xI (xI (xI (xO (xI p)))))
-  | "L"%char => xI (xI (xI (xI (xO (xI p)))))
-  | "M"%char => xO (xO (xO (xO (xI (xI p)))))
-  | "N"%char => xI (xO (xO (xO (xI (xI p)))))
-  | "O"%char => xO (xI (xO (xO (xI (xI p)))))
-  | "P"%char => xI (xI (xO (xO (xI (xI p)))))
-  | "Q"%char => xO (xO (xI (xO (xI (xI p)))))
-  | "R"%char => xI (xO (xI (xO (xI (xI p)))))
-  | "S"%char => xO (xI (xI (xO (xI (xI p)))))
-  | "T"%char => xI (xI (xI (xO (xI (xI p)))))
-  | "U"%char => xO (xO (xO (xI (xI (xI p)))))
-  | "V"%char => xI (xO (xO (xI (xI (xI p)))))
-  | "W"%char => xO (xI (xO (xI (xI (xI p)))))
-  | "X"%char => xI (xI (xO (xI (xI (xI p)))))
-  | "Y"%char => xO (xO (xI (xI (xI (xI p)))))
-  | "Z"%char => xI (xO (xI (xI (xI (xI p)))))
-  | "_"%char => xO (xI (xI (xI (xI (xI p)))))
-  | _ => append_char_pos_default c p
-  end.
-
-Fixpoint ident_of_string (s: string) : ident :=
-  match s with
-  | EmptyString => xH
-  | String c s => append_char_pos c (ident_of_string s)
-  end.
-
-(** The inverse conversion, from encoded strings to strings *)
-
-Section DECODE_BITS.
-
-Variable rec: positive -> string.
-
-Fixpoint decode_n_bits (n: nat) (l: list bool) (p: positive) : string :=
-  match n with
-  | O => 
-      match l with 
-      | b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: _ =>
-          String (Ascii b7 b6 b5 b4 b3 b2 b1 b0) (rec p)
-      | _ => EmptyString
-      end
-  | S n =>
-      match p with
-      | xO q => decode_n_bits n (false :: l) q
-      | xI q => decode_n_bits n (true :: l) q
-      | xH => EmptyString
-      end
-  end.
-
-Definition decode_8_bits := Eval compute in (decode_n_bits 8%nat nil).
-
-End DECODE_BITS.
-
-Fixpoint string_of_ident (p: positive) : string :=
-  match p with
-  | xO (xO (xO (xO (xO (xO p))))) => String "0"%char (string_of_ident p)
-  | xI (xO (xO (xO (xO (xO p))))) => String "1"%char (string_of_ident p)
-  | xO (xI (xO (xO (xO (xO p))))) => String "2"%char (string_of_ident p)
-  | xI (xI (xO (xO (xO (xO p))))) => String "3"%char (string_of_ident p)
-  | xO (xO (xI (xO (xO (xO p))))) => String "4"%char (string_of_ident p)
-  | xI (xO (xI (xO (xO (xO p))))) => String "5"%char (string_of_ident p)
-  | xO (xI (xI (xO (xO (xO p))))) => String "6"%char (string_of_ident p)
-  | xI (xI (xI (xO (xO (xO p))))) => String "7"%char (string_of_ident p)
-  | xO (xO (xO (xI (xO (xO p))))) => String "8"%char (string_of_ident p)
-  | xI (xO (xO (xI (xO (xO p))))) => String "9"%char (string_of_ident p)
-  | xO (xI (xO (xI (xO (xO p))))) => String "a"%char (string_of_ident p)
-  | xI (xI (xO (xI (xO (xO p))))) => String "b"%char (string_of_ident p)
-  | xO (xO (xI (xI (xO (xO p))))) => String "c"%char (string_of_ident p)
-  | xI (xO (xI (xI (xO (xO p))))) => String "d"%char (string_of_ident p)
-  | xO (xI (xI (xI (xO (xO p))))) => String "e"%char (string_of_ident p)
-  | xI (xI (xI (xI (xO (xO p))))) => String "f"%char (string_of_ident p)
-  | xO (xO (xO (xO (xI (xO p))))) => String "g"%char (string_of_ident p)
-  | xI (xO (xO (xO (xI (xO p))))) => String "h"%char (string_of_ident p)
-  | xO (xI (xO (xO (xI (xO p))))) => String "i"%char (string_of_ident p)
-  | xI (xI (xO (xO (xI (xO p))))) => String "j"%char (string_of_ident p)
-  | xO (xO (xI (xO (xI (xO p))))) => String "k"%char (string_of_ident p)
-  | xI (xO (xI (xO (xI (xO p))))) => String "l"%char (string_of_ident p)
-  | xO (xI (xI (xO (xI (xO p))))) => String "m"%char (string_of_ident p)
-  | xI (xI (xI (xO (xI (xO p))))) => String "n"%char (string_of_ident p)
-  | xO (xO (xO (xI (xI (xO p))))) => String "o"%char (string_of_ident p)
-  | xI (xO (xO (xI (xI (xO p))))) => String "p"%char (string_of_ident p)
-  | xO (xI (xO (xI (xI (xO p))))) => String "q"%char (string_of_ident p)
-  | xI (xI (xO (xI (xI (xO p))))) => String "r"%char (string_of_ident p)
-  | xO (xO (xI (xI (xI (xO p))))) => String "s"%char (string_of_ident p)
-  | xI (xO (xI (xI (xI (xO p))))) => String "t"%char (string_of_ident p)
-  | xO (xI (xI (xI (xI (xO p))))) => String "u"%char (string_of_ident p)
-  | xI (xI (xI (xI (xI (xO p))))) => String "v"%char (string_of_ident p)
-  | xO (xO (xO (xO (xO (xI p))))) => String "w"%char (string_of_ident p)
-  | xI (xO (xO (xO (xO (xI p))))) => String "x"%char (string_of_ident p)
-  | xO (xI (xO (xO (xO (xI p))))) => String "y"%char (string_of_ident p)
-  | xI (xI (xO (xO (xO (xI p))))) => String "z"%char (string_of_ident p)
-  | xO (xO (xI (xO (xO (xI p))))) => String "A"%char (string_of_ident p)
-  | xI (xO (xI (xO (xO (xI p))))) => String "B"%char (string_of_ident p)
-  | xO (xI (xI (xO (xO (xI p))))) => String "C"%char (string_of_ident p)
-  | xI (xI (xI (xO (xO (xI p))))) => String "D"%char (string_of_ident p)
-  | xO (xO (xO (xI (xO (xI p))))) => String "E"%char (string_of_ident p)
-  | xI (xO (xO (xI (xO (xI p))))) => String "F"%char (string_of_ident p)
-  | xO (xI (xO (xI (xO (xI p))))) => String "G"%char (string_of_ident p)
-  | xI (xI (xO (xI (xO (xI p))))) => String "H"%char (string_of_ident p)
-  | xO (xO (xI (xI (xO (xI p))))) => String "I"%char (string_of_ident p)
-  | xI (xO (xI (xI (xO (xI p))))) => String "J"%char (string_of_ident p)
-  | xO (xI (xI (xI (xO (xI p))))) => String "K"%char (string_of_ident p)
-  | xI (xI (xI (xI (xO (xI p))))) => String "L"%char (string_of_ident p)
-  | xO (xO (xO (xO (xI (xI p))))) => String "M"%char (string_of_ident p)
-  | xI (xO (xO (xO (xI (xI p))))) => String "N"%char (string_of_ident p)
-  | xO (xI (xO (xO (xI (xI p))))) => String "O"%char (string_of_ident p)
-  | xI (xI (xO (xO (xI (xI p))))) => String "P"%char (string_of_ident p)
-  | xO (xO (xI (xO (xI (xI p))))) => String "Q"%char (string_of_ident p)
-  | xI (xO (xI (xO (xI (xI p))))) => String "R"%char (string_of_ident p)
-  | xO (xI (xI (xO (xI (xI p))))) => String "S"%char (string_of_ident p)
-  | xI (xI (xI (xO (xI (xI p))))) => String "T"%char (string_of_ident p)
-  | xO (xO (xO (xI (xI (xI p))))) => String "U"%char (string_of_ident p)
-  | xI (xO (xO (xI (xI (xI p))))) => String "V"%char (string_of_ident p)
-  | xO (xI (xO (xI (xI (xI p))))) => String "W"%char (string_of_ident p)
-  | xI (xI (xO (xI (xI (xI p))))) => String "X"%char (string_of_ident p)
-  | xO (xO (xI (xI (xI (xI p))))) => String "Y"%char (string_of_ident p)
-  | xI (xO (xI (xI (xI (xI p))))) => String "Z"%char (string_of_ident p)
-  | xO (xI (xI (xI (xI (xI p))))) => String "_"%char (string_of_ident p)
-  | xI (xI (xI (xI (xI (xI p))))) => decode_8_bits string_of_ident p
-  | _ => EmptyString
-  end.
-
-Lemma string_of_ident_of_string:
-  forall s, string_of_ident (ident_of_string s) = s.
-Proof.
-  induction s as [ | c s]; simpl.
-- auto.
-- rewrite <- IHs at 2. destruct c as [[] [] [] [] [] [] [] []]; reflexivity.
-Qed.
-
-Corollary ident_of_string_injective:
-  forall s1 s2, ident_of_string s1 = ident_of_string s2 -> s1 = s2.
-Proof.
-  intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2).
-  congruence.
-Qed.
-
 (** ** Notations *)
 
 Module ClightNotations.
diff --git a/export/Csyntaxdefs.v b/export/Csyntaxdefs.v
new file mode 100644
index 00000000..84ce9f3a
--- /dev/null
+++ b/export/Csyntaxdefs.v
@@ -0,0 +1,65 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 Lesser General Public License as        *)
+(*  published by the Free Software Foundation, either version 2.1 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.                            *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Definitions used by .v files generated by clightgen -csyntax *)
+
+From Coq Require Import List.
+From compcert Require Import Maps Errors AST Ctypes Csyntax.
+From compcert Require Export Ctypesdefs.
+
+(** ** Constructor for programs and compilation units *)
+
+Definition wf_composites (types: list composite_definition) : Prop :=
+  match build_composite_env types with OK _ => True | Error _ => False end.
+
+Definition build_composite_env' (types: list composite_definition)
+                                (WF: wf_composites types)
+                             : { ce | build_composite_env types  = OK ce }.
+Proof.
+  revert WF. unfold wf_composites. case (build_composite_env types); intros.
+- exists c; reflexivity.
+- contradiction.
+Defined.
+
+Definition mkprogram (types: list composite_definition)
+                     (defs: list (ident * globdef fundef type))
+                     (public: list ident)
+                     (main: ident)
+                     (WF: wf_composites types) : Csyntax.program :=
+  let (ce, EQ) := build_composite_env' types WF in
+  {| prog_defs := defs;
+     prog_public := public;
+     prog_main := main;
+     prog_types := types;
+     prog_comp_env := ce;
+     prog_comp_env_eq := EQ |}.
+
+(** ** Notations *)
+
+Module CsyntaxNotations.
+
+(** A convenient notation [$ "ident"] to force evaluation of
+    [ident_of_string "ident"] *)
+
+Ltac ident_of_string s :=
+  let x := constr:(ident_of_string s) in
+  let y := eval compute in x in
+  exact y.
+
+Notation "$ s" := (ltac:(ident_of_string s))
+                  (at level 1, only parsing) : csyntax_scope.
+
+End CsyntaxNotations.
diff --git a/export/Ctypesdefs.v b/export/Ctypesdefs.v
new file mode 100644
index 00000000..45695ebb
--- /dev/null
+++ b/export/Ctypesdefs.v
@@ -0,0 +1,260 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 Lesser General Public License as        *)
+(*  published by the Free Software Foundation, either version 2.1 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.                            *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Definitions used by the .v files generated by clightgen *)
+
+From Coq Require Import Ascii String List ZArith.
+From compcert Require Import Maps Errors AST Ctypes.
+
+(** ** Short names for types *)
+
+Definition tvoid := Tvoid.
+Definition tschar := Tint I8 Signed noattr.
+Definition tuchar := Tint I8 Unsigned noattr.
+Definition tshort := Tint I16 Signed noattr.
+Definition tushort := Tint I16 Unsigned noattr.
+Definition tint := Tint I32 Signed noattr.
+Definition tuint := Tint I32 Unsigned noattr.
+Definition tbool := Tint IBool Unsigned noattr.
+Definition tlong := Tlong Signed noattr.
+Definition tulong := Tlong Unsigned noattr.
+Definition tfloat := Tfloat F32 noattr.
+Definition tdouble := Tfloat F64 noattr.
+Definition tptr (t: type) := Tpointer t noattr.
+Definition tarray (t: type) (sz: Z) := Tarray t sz noattr.
+
+Definition volatile_attr := {| attr_volatile := true; attr_alignas := None |}.
+
+Definition tattr (a: attr) (ty: type) :=
+  match ty with
+  | Tvoid => Tvoid
+  | Tint sz si _ => Tint sz si a
+  | Tlong si _ => Tlong si a
+  | Tfloat sz _ => Tfloat sz a
+  | Tpointer elt _ => Tpointer elt a
+  | Tarray elt sz _ => Tarray elt sz a
+  | Tfunction args res cc => Tfunction args res cc
+  | Tstruct id _ => Tstruct id a
+  | Tunion id  _ => Tunion id a
+  end.
+
+Definition tvolatile (ty: type) := tattr volatile_attr ty.
+
+Definition talignas (n: N) (ty: type) :=
+  tattr {| attr_volatile := false; attr_alignas := Some n |} ty.
+
+Definition tvolatile_alignas (n: N) (ty: type) :=
+  tattr {| attr_volatile := true; attr_alignas := Some n |} ty.
+
+(** ** Encoding character strings as positive numbers *)
+
+(** The following encoding of character strings as positive numbers
+    must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *)
+
+Definition append_bit_pos (b: bool) (p: positive) : positive :=
+  if b then xI p else xO p.
+
+Definition append_char_pos_default (c: ascii) (p: positive) : positive :=
+  let '(Ascii b7 b6 b5 b4 b3 b2 b1 b0) := c in
+  xI (xI (xI (xI (xI (xI
+    (append_bit_pos b0 (append_bit_pos b1
+    (append_bit_pos b2 (append_bit_pos b3
+    (append_bit_pos b4 (append_bit_pos b5
+    (append_bit_pos b6 (append_bit_pos b7 p))))))))))))).
+
+Definition append_char_pos (c: ascii) (p: positive) : positive :=
+  match c with
+  | "0"%char => xO (xO (xO (xO (xO (xO p)))))
+  | "1"%char => xI (xO (xO (xO (xO (xO p)))))
+  | "2"%char => xO (xI (xO (xO (xO (xO p)))))
+  | "3"%char => xI (xI (xO (xO (xO (xO p)))))
+  | "4"%char => xO (xO (xI (xO (xO (xO p)))))
+  | "5"%char => xI (xO (xI (xO (xO (xO p)))))
+  | "6"%char => xO (xI (xI (xO (xO (xO p)))))
+  | "7"%char => xI (xI (xI (xO (xO (xO p)))))
+  | "8"%char => xO (xO (xO (xI (xO (xO p)))))
+  | "9"%char => xI (xO (xO (xI (xO (xO p)))))
+  | "a"%char => xO (xI (xO (xI (xO (xO p)))))
+  | "b"%char => xI (xI (xO (xI (xO (xO p)))))
+  | "c"%char => xO (xO (xI (xI (xO (xO p)))))
+  | "d"%char => xI (xO (xI (xI (xO (xO p)))))
+  | "e"%char => xO (xI (xI (xI (xO (xO p)))))
+  | "f"%char => xI (xI (xI (xI (xO (xO p)))))
+  | "g"%char => xO (xO (xO (xO (xI (xO p)))))
+  | "h"%char => xI (xO (xO (xO (xI (xO p)))))
+  | "i"%char => xO (xI (xO (xO (xI (xO p)))))
+  | "j"%char => xI (xI (xO (xO (xI (xO p)))))
+  | "k"%char => xO (xO (xI (xO (xI (xO p)))))
+  | "l"%char => xI (xO (xI (xO (xI (xO p)))))
+  | "m"%char => xO (xI (xI (xO (xI (xO p)))))
+  | "n"%char => xI (xI (xI (xO (xI (xO p)))))
+  | "o"%char => xO (xO (xO (xI (xI (xO p)))))
+  | "p"%char => xI (xO (xO (xI (xI (xO p)))))
+  | "q"%char => xO (xI (xO (xI (xI (xO p)))))
+  | "r"%char => xI (xI (xO (xI (xI (xO p)))))
+  | "s"%char => xO (xO (xI (xI (xI (xO p)))))
+  | "t"%char => xI (xO (xI (xI (xI (xO p)))))
+  | "u"%char => xO (xI (xI (xI (xI (xO p)))))
+  | "v"%char => xI (xI (xI (xI (xI (xO p)))))
+  | "w"%char => xO (xO (xO (xO (xO (xI p)))))
+  | "x"%char => xI (xO (xO (xO (xO (xI p)))))
+  | "y"%char => xO (xI (xO (xO (xO (xI p)))))
+  | "z"%char => xI (xI (xO (xO (xO (xI p)))))
+  | "A"%char => xO (xO (xI (xO (xO (xI p)))))
+  | "B"%char => xI (xO (xI (xO (xO (xI p)))))
+  | "C"%char => xO (xI (xI (xO (xO (xI p)))))
+  | "D"%char => xI (xI (xI (xO (xO (xI p)))))
+  | "E"%char => xO (xO (xO (xI (xO (xI p)))))
+  | "F"%char => xI (xO (xO (xI (xO (xI p)))))
+  | "G"%char => xO (xI (xO (xI (xO (xI p)))))
+  | "H"%char => xI (xI (xO (xI (xO (xI p)))))
+  | "I"%char => xO (xO (xI (xI (xO (xI p)))))
+  | "J"%char => xI (xO (xI (xI (xO (xI p)))))
+  | "K"%char => xO (xI (xI (xI (xO (xI p)))))
+  | "L"%char => xI (xI (xI (xI (xO (xI p)))))
+  | "M"%char => xO (xO (xO (xO (xI (xI p)))))
+  | "N"%char => xI (xO (xO (xO (xI (xI p)))))
+  | "O"%char => xO (xI (xO (xO (xI (xI p)))))
+  | "P"%char => xI (xI (xO (xO (xI (xI p)))))
+  | "Q"%char => xO (xO (xI (xO (xI (xI p)))))
+  | "R"%char => xI (xO (xI (xO (xI (xI p)))))
+  | "S"%char => xO (xI (xI (xO (xI (xI p)))))
+  | "T"%char => xI (xI (xI (xO (xI (xI p)))))
+  | "U"%char => xO (xO (xO (xI (xI (xI p)))))
+  | "V"%char => xI (xO (xO (xI (xI (xI p)))))
+  | "W"%char => xO (xI (xO (xI (xI (xI p)))))
+  | "X"%char => xI (xI (xO (xI (xI (xI p)))))
+  | "Y"%char => xO (xO (xI (xI (xI (xI p)))))
+  | "Z"%char => xI (xO (xI (xI (xI (xI p)))))
+  | "_"%char => xO (xI (xI (xI (xI (xI p)))))
+  | _ => append_char_pos_default c p
+  end.
+
+Fixpoint ident_of_string (s: string) : ident :=
+  match s with
+  | EmptyString => xH
+  | String c s => append_char_pos c (ident_of_string s)
+  end.
+
+(** The inverse conversion, from encoded strings to strings *)
+
+Section DECODE_BITS.
+
+Variable rec: positive -> string.
+
+Fixpoint decode_n_bits (n: nat) (l: list bool) (p: positive) : string :=
+  match n with
+  | O => 
+      match l with 
+      | b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: _ =>
+          String (Ascii b7 b6 b5 b4 b3 b2 b1 b0) (rec p)
+      | _ => EmptyString
+      end
+  | S n =>
+      match p with
+      | xO q => decode_n_bits n (false :: l) q
+      | xI q => decode_n_bits n (true :: l) q
+      | xH => EmptyString
+      end
+  end.
+
+Definition decode_8_bits := Eval compute in (decode_n_bits 8%nat nil).
+
+End DECODE_BITS.
+
+Fixpoint string_of_ident (p: positive) : string :=
+  match p with
+  | xO (xO (xO (xO (xO (xO p))))) => String "0"%char (string_of_ident p)
+  | xI (xO (xO (xO (xO (xO p))))) => String "1"%char (string_of_ident p)
+  | xO (xI (xO (xO (xO (xO p))))) => String "2"%char (string_of_ident p)
+  | xI (xI (xO (xO (xO (xO p))))) => String "3"%char (string_of_ident p)
+  | xO (xO (xI (xO (xO (xO p))))) => String "4"%char (string_of_ident p)
+  | xI (xO (xI (xO (xO (xO p))))) => String "5"%char (string_of_ident p)
+  | xO (xI (xI (xO (xO (xO p))))) => String "6"%char (string_of_ident p)
+  | xI (xI (xI (xO (xO (xO p))))) => String "7"%char (string_of_ident p)
+  | xO (xO (xO (xI (xO (xO p))))) => String "8"%char (string_of_ident p)
+  | xI (xO (xO (xI (xO (xO p))))) => String "9"%char (string_of_ident p)
+  | xO (xI (xO (xI (xO (xO p))))) => String "a"%char (string_of_ident p)
+  | xI (xI (xO (xI (xO (xO p))))) => String "b"%char (string_of_ident p)
+  | xO (xO (xI (xI (xO (xO p))))) => String "c"%char (string_of_ident p)
+  | xI (xO (xI (xI (xO (xO p))))) => String "d"%char (string_of_ident p)
+  | xO (xI (xI (xI (xO (xO p))))) => String "e"%char (string_of_ident p)
+  | xI (xI (xI (xI (xO (xO p))))) => String "f"%char (string_of_ident p)
+  | xO (xO (xO (xO (xI (xO p))))) => String "g"%char (string_of_ident p)
+  | xI (xO (xO (xO (xI (xO p))))) => String "h"%char (string_of_ident p)
+  | xO (xI (xO (xO (xI (xO p))))) => String "i"%char (string_of_ident p)
+  | xI (xI (xO (xO (xI (xO p))))) => String "j"%char (string_of_ident p)
+  | xO (xO (xI (xO (xI (xO p))))) => String "k"%char (string_of_ident p)
+  | xI (xO (xI (xO (xI (xO p))))) => String "l"%char (string_of_ident p)
+  | xO (xI (xI (xO (xI (xO p))))) => String "m"%char (string_of_ident p)
+  | xI (xI (xI (xO (xI (xO p))))) => String "n"%char (string_of_ident p)
+  | xO (xO (xO (xI (xI (xO p))))) => String "o"%char (string_of_ident p)
+  | xI (xO (xO (xI (xI (xO p))))) => String "p"%char (string_of_ident p)
+  | xO (xI (xO (xI (xI (xO p))))) => String "q"%char (string_of_ident p)
+  | xI (xI (xO (xI (xI (xO p))))) => String "r"%char (string_of_ident p)
+  | xO (xO (xI (xI (xI (xO p))))) => String "s"%char (string_of_ident p)
+  | xI (xO (xI (xI (xI (xO p))))) => String "t"%char (string_of_ident p)
+  | xO (xI (xI (xI (xI (xO p))))) => String "u"%char (string_of_ident p)
+  | xI (xI (xI (xI (xI (xO p))))) => String "v"%char (string_of_ident p)
+  | xO (xO (xO (xO (xO (xI p))))) => String "w"%char (string_of_ident p)
+  | xI (xO (xO (xO (xO (xI p))))) => String "x"%char (string_of_ident p)
+  | xO (xI (xO (xO (xO (xI p))))) => String "y"%char (string_of_ident p)
+  | xI (xI (xO (xO (xO (xI p))))) => String "z"%char (string_of_ident p)
+  | xO (xO (xI (xO (xO (xI p))))) => String "A"%char (string_of_ident p)
+  | xI (xO (xI (xO (xO (xI p))))) => String "B"%char (string_of_ident p)
+  | xO (xI (xI (xO (xO (xI p))))) => String "C"%char (string_of_ident p)
+  | xI (xI (xI (xO (xO (xI p))))) => String "D"%char (string_of_ident p)
+  | xO (xO (xO (xI (xO (xI p))))) => String "E"%char (string_of_ident p)
+  | xI (xO (xO (xI (xO (xI p))))) => String "F"%char (string_of_ident p)
+  | xO (xI (xO (xI (xO (xI p))))) => String "G"%char (string_of_ident p)
+  | xI (xI (xO (xI (xO (xI p))))) => String "H"%char (string_of_ident p)
+  | xO (xO (xI (xI (xO (xI p))))) => String "I"%char (string_of_ident p)
+  | xI (xO (xI (xI (xO (xI p))))) => String "J"%char (string_of_ident p)
+  | xO (xI (xI (xI (xO (xI p))))) => String "K"%char (string_of_ident p)
+  | xI (xI (xI (xI (xO (xI p))))) => String "L"%char (string_of_ident p)
+  | xO (xO (xO (xO (xI (xI p))))) => String "M"%char (string_of_ident p)
+  | xI (xO (xO (xO (xI (xI p))))) => String "N"%char (string_of_ident p)
+  | xO (xI (xO (xO (xI (xI p))))) => String "O"%char (string_of_ident p)
+  | xI (xI (xO (xO (xI (xI p))))) => String "P"%char (string_of_ident p)
+  | xO (xO (xI (xO (xI (xI p))))) => String "Q"%char (string_of_ident p)
+  | xI (xO (xI (xO (xI (xI p))))) => String "R"%char (string_of_ident p)
+  | xO (xI (xI (xO (xI (xI p))))) => String "S"%char (string_of_ident p)
+  | xI (xI (xI (xO (xI (xI p))))) => String "T"%char (string_of_ident p)
+  | xO (xO (xO (xI (xI (xI p))))) => String "U"%char (string_of_ident p)
+  | xI (xO (xO (xI (xI (xI p))))) => String "V"%char (string_of_ident p)
+  | xO (xI (xO (xI (xI (xI p))))) => String "W"%char (string_of_ident p)
+  | xI (xI (xO (xI (xI (xI p))))) => String "X"%char (string_of_ident p)
+  | xO (xO (xI (xI (xI (xI p))))) => String "Y"%char (string_of_ident p)
+  | xI (xO (xI (xI (xI (xI p))))) => String "Z"%char (string_of_ident p)
+  | xO (xI (xI (xI (xI (xI p))))) => String "_"%char (string_of_ident p)
+  | xI (xI (xI (xI (xI (xI p))))) => decode_8_bits string_of_ident p
+  | _ => EmptyString
+  end.
+
+Lemma string_of_ident_of_string:
+  forall s, string_of_ident (ident_of_string s) = s.
+Proof.
+  induction s as [ | c s]; simpl.
+- auto.
+- rewrite <- IHs at 2. destruct c as [[] [] [] [] [] [] [] []]; reflexivity.
+Qed.
+
+Corollary ident_of_string_injective:
+  forall s1 s2, ident_of_string s1 = ident_of_string s2 -> s1 = s2.
+Proof.
+  intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2).
+  congruence.
+Qed.
diff --git a/export/ExportBase.ml b/export/ExportBase.ml
index b7d0170d..4b93d8a9 100644
--- a/export/ExportBase.ml
+++ b/export/ExportBase.ml
@@ -17,6 +17,7 @@
 open Format
 open Camlcoq
 open AST
+open Values
 
 (* Options, lists, pairs *)
 
@@ -239,9 +240,19 @@ let print_variable print_info p (id, v) =
   fprintf p "  gvar_volatile := %B@ " v.gvar_volatile;
   fprintf p "|}.@ @ "
 
-(* Information about this run of clightgen *)
+(* Values *)
 
-let print_clightgen_info ~sourcefile ?normalized p =
+let val_ p = function
+  | Vundef -> fprintf p "Vundef"
+  | Vint i -> fprintf p "(Vint %a)" coqint i
+  | Vlong l -> fprintf p "(Vlong %a)" coqint64 l
+  | Vfloat f -> fprintf p "(Vfloat %a)" coqfloat f
+  | Vsingle s -> fprintf p "(Vsingle %a)" coqsingle s
+  | Vptr(b, o) -> fprintf p "(Vptr %a %a)" positive b coqptrofs o
+
+(* Information about this run of clightgen or csyntaxgen *)
+
+let print_gen_info ~sourcefile ?normalized p =
   fprintf p "@[<v 2>Module Info.";
   fprintf p "@ Definition version := %S." Version.version;
   fprintf p "@ Definition build_number := %S." Version.buildnr;
diff --git a/export/ExportClight.ml b/export/ExportClight.ml
index 421db5ed..e3b00986 100644
--- a/export/ExportClight.ml
+++ b/export/ExportClight.ml
@@ -233,7 +233,7 @@ let print_program p prog sourcefile normalized =
   name_program prog;
   fprintf p "@[<v 0>";
   fprintf p "%s" prologue;
-  print_clightgen_info ~sourcefile ~normalized p;
+  print_gen_info ~sourcefile ~normalized p;
   define_idents p;
   List.iter (print_globdef p) prog.Ctypes.prog_defs;
   fprintf p "Definition composites : list composite_definition :=@ ";
diff --git a/export/ExportCsyntax.ml b/export/ExportCsyntax.ml
new file mode 100644
index 00000000..1d91cba5
--- /dev/null
+++ b/export/ExportCsyntax.ml
@@ -0,0 +1,209 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bart Jacobs, KU Leuven                                     *)
+(*          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 Lesser General Public License as        *)
+(*  published by the Free Software Foundation, either version 2.1 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.                            *)
+(*                                                                     *)
+(*  The contributions by Bart Jacobs are reused and adapted            *)
+(*  under the terms of a Contributor License Agreement.                *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Export C syntax as a Coq file *)
+
+open Format
+open Camlcoq
+open AST
+open! Ctypes
+open Cop
+open Csyntax
+open ExportBase
+open ExportCtypes
+
+(* Expressions *)
+
+let name_unop = function
+  | Onotbool -> "Onotbool"
+  | Onotint -> "Onotint"
+  | Oneg -> "Oneg"
+  | Oabsfloat -> "Oabsfloat"
+
+let name_binop = function
+  | Oadd -> "Oadd"
+  | Osub -> "Osub"
+  | Omul -> "Omul"
+  | Odiv -> "Odiv"
+  | Omod -> "Omod"
+  | Oand -> "Oand"
+  | Oor -> "Oor"
+  | Oxor -> "Oxor"
+  | Oshl -> "Oshl"
+  | Oshr -> "Oshr"
+  | Oeq -> "Oeq"
+  | Cop.One -> "One"
+  | Olt -> "Olt"
+  | Ogt -> "Ogt"
+  | Ole -> "Ole"
+  | Oge -> "Oge"
+
+let name_incr_or_decr = function
+  | Incr -> "Incr"
+  | Decr -> "Decr"
+
+let rec expr p = function
+  | Eval(v, t) ->
+      fprintf p "(Eval %a %a)" val_ v typ t
+  | Evar(id, t) ->
+      fprintf p "(Evar %a %a)" ident id typ t
+  | Efield(a1, f, t) ->
+      fprintf p "@[<hov 2>(Efield@ %a@ %a@ %a)@]" expr a1 ident f typ t
+  | Evalof(l, t) ->
+      fprintf p "@[<hov 2>(Evalof@ %a@ %a)@]" expr l typ t
+  | Ederef(a1, t) ->
+      fprintf p "@[<hov 2>(Ederef@ %a@ %a)@]" expr a1 typ t
+  | Eaddrof(a1, t) ->
+      fprintf p "@[<hov 2>(Eaddrof@ %a@ %a)@]" expr a1 typ t
+  | Eunop(op, a1, t) ->
+      fprintf p "@[<hov 2>(Eunop %s@ %a@ %a)@]"
+         (name_unop op) expr a1 typ t
+  | Ebinop(op, a1, a2, t) ->
+      fprintf p "@[<hov 2>(Ebinop %s@ %a@ %a@ %a)@]"
+         (name_binop op) expr a1 expr a2 typ t
+  | Ecast(a1, t) ->
+      fprintf p "@[<hov 2>(Ecast@ %a@ %a)@]" expr a1 typ t
+  | Eseqand(a1, a2, t) ->
+      fprintf p "@[<hov 2>(Eseqand@ %a@ %a@ %a)@]" expr a1 expr a2 typ t
+  | Eseqor(a1, a2, t) ->
+      fprintf p "@[<hov 2>(Eseqor@ %a@ %a@ %a)@]" expr a1 expr a2 typ t
+  | Econdition(a1, a2, a3, t) ->
+      fprintf p "@[<hov 2>(Econdition@ %a@ %a@ %a@ %a)@]" expr a1 expr a2 expr a3 typ t
+  | Esizeof(t1, t) ->
+      fprintf p "(Esizeof %a %a)" typ t1 typ t
+  | Ealignof(t1, t) ->
+      fprintf p "(Ealignof %a %a)" typ t1 typ t
+  | Eassign(l, r, t) ->
+      fprintf p "@[<hov 2>(Eassign@ %a@ %a@ %a)@]" expr l expr r typ t
+  | Eassignop(op, l, r, t', t) ->
+      fprintf p "@[<hov 2>(Eassignop@ %s@ %a@ %a@ %a %a)@]" (name_binop op) expr l expr r typ t' typ t
+  | Epostincr(id, l, t) ->
+      fprintf p "@[<hov 2>(Epostincr@ %s@ %a@ %a)@]" (name_incr_or_decr id) expr l typ t
+  | Ecomma(a1, a2, t) ->
+      fprintf p "@[<hov 2>(Ecomma@ %a@ %a@ %a)@]" expr a1 expr a2 typ t
+  | Ecall(r1, rargs, t) ->
+      fprintf p "@[<hov 2>(Ecall@ %a@ %a@ %a)@]" expr r1 exprlist rargs typ t
+  | Ebuiltin(ef, tyargs, rargs, t) ->
+      fprintf p "@[<hov 2>(Ebuiltin@ %a@ %a@ %a@ %a)@]" external_function ef typlist tyargs exprlist rargs typ t
+  | Eloc(b, o, bf, t) ->
+      fprintf p "@[<hov 2>(Eloc@ %a@ %a@ %a@ %a)@]" positive b coqptrofs o bitfield bf typ t
+  | Eparen(r, t', t) ->
+      fprintf p "@[<hov 2>(Eparen@ %a@ %a@ %a)@]" expr r typ t' typ t
+and exprlist p = function
+  | Enil ->
+      fprintf p "Enil"
+  | Econs(r1, rl) ->
+      fprintf p "@[<hov 2>(Econs@ %a@ %a)@]" expr r1 exprlist rl
+
+(* Statements *)
+
+let rec statement p = function
+  | Sskip ->
+      fprintf p "Sskip"
+  | Sdo(e) ->
+      fprintf p "@[<hv 2>(Sdo %a)@]" expr e
+  | Ssequence(s1, s2) ->
+      fprintf p "@[<hv 2>(Ssequence@ %a@ %a)@]" statement s1 statement s2
+  | Sifthenelse(e, s1, s2) ->
+      fprintf p "@[<hv 2>(Sifthenelse %a@ %a@ %a)@]" expr e statement s1 statement s2
+  | Swhile(e, s) ->
+      fprintf p "@[<hv 2>(Swhile@ %a@ %a)@]" expr e statement s
+  | Sdowhile(e, s) ->
+      fprintf p "@[<hv 2>(Sdowhile@ %a@ %a)@]" expr e statement s
+  | Sfor(s1, e, s2, s3) ->
+      fprintf p "@[<hv 2>(Sfor@ %a@ %a@ %a@ %a)@]" statement s1 expr e statement s2 statement s3
+  | Sbreak ->
+      fprintf p "Sbreak"
+  | Scontinue ->
+      fprintf p "Scontinue"
+  | Sreturn e ->
+      fprintf p "@[<hv 2>(Sreturn %a)@]" (print_option expr) e
+  | Sswitch(e, cases) ->
+      fprintf p "@[<hv 2>(Sswitch %a@ %a)@]" expr e labeled_statements cases
+  | Slabel(lbl, s1) ->
+      fprintf p "@[<hv 2>(Slabel %a@ %a)@]" ident lbl statement s1
+  | Sgoto lbl ->
+      fprintf p "(Sgoto %a)" ident lbl
+
+and labeled_statements p = function
+  | LSnil ->
+      (fprintf p "LSnil")
+  | LScons(lbl, s, ls) ->
+      fprintf p "@[<hv 2>(LScons %a@ %a@ %a)@]"
+              (print_option coqZ) lbl statement s labeled_statements ls
+
+(* Global definitions *)
+
+let print_function p (id, f) =
+  fprintf p "Definition f%s := {|@ " (sanitize (extern_atom id));
+  fprintf p "  fn_return := %a;@ " typ f.fn_return;
+  fprintf p "  fn_callconv := %a;@ " callconv f.fn_callconv;
+  fprintf p "  fn_params := %a;@ " (print_list (print_pair ident typ)) f.fn_params;
+  fprintf p "  fn_vars := %a;@ " (print_list (print_pair ident typ)) f.fn_vars;
+  fprintf p "  fn_body :=@ ";
+  statement p f.fn_body;
+  fprintf p "@ |}.@ @ "
+
+let print_globdef p (id, gd) =
+  match gd with
+  | Gfun(Ctypes.Internal f) -> print_function p (id, f)
+  | Gfun(Ctypes.External _) -> ()
+  | Gvar v -> print_variable typ p (id, v)
+
+let print_ident_globdef p = function
+  | (id, Gfun(Ctypes.Internal f)) ->
+      fprintf p "(%a, Gfun(Internal f%s))" ident id (sanitize (extern_atom id))
+  | (id, Gfun(Ctypes.External(ef, targs, tres, cc))) ->
+      fprintf p "@[<hov 2>(%a,@ @[<hov 2>Gfun(External %a@ %a@ %a@ %a))@]@]"
+        ident id external_function ef typlist targs typ tres callconv cc
+  | (id, Gvar v) ->
+      fprintf p "(%a, Gvar v%s)" ident id (sanitize (extern_atom id))
+
+(* The prologue *)
+
+let prologue = "\
+From Coq Require Import String List ZArith.\n\
+From compcert Require Import Coqlib Integers Floats Values AST Ctypes Cop Csyntax Csyntaxdefs.\n\
+Import Csyntaxdefs.CsyntaxNotations.\n\
+Local Open Scope Z_scope.\n\
+Local Open Scope string_scope.\n\
+Local Open Scope csyntax_scope.\n"
+
+(* All together *)
+
+let print_program p prog sourcefile =
+  fprintf p "@[<v 0>";
+  fprintf p "%s" prologue;
+  print_gen_info ~sourcefile p;
+  define_idents p;
+  List.iter (print_globdef p) prog.Ctypes.prog_defs;
+  fprintf p "Definition composites : list composite_definition :=@ ";
+  print_list print_composite_definition p prog.prog_types;
+  fprintf p ".@ @ ";
+  fprintf p "Definition global_definitions : list (ident * globdef fundef type) :=@ ";
+  print_list print_ident_globdef p prog.Ctypes.prog_defs;
+  fprintf p ".@ @ ";
+  fprintf p "Definition public_idents : list ident :=@ ";
+  print_list ident p prog.Ctypes.prog_public;
+  fprintf p ".@ @ ";
+  fprintf p "Definition prog : Csyntax.program := @ ";
+  fprintf p "  mkprogram composites global_definitions public_idents %a Logic.I.@ @ "
+            ident prog.Ctypes.prog_main;
+  fprintf p "@]@."
diff --git a/export/ExportCtypes.ml b/export/ExportCtypes.ml
index 428a1459..d0a7f28a 100644
--- a/export/ExportCtypes.ml
+++ b/export/ExportCtypes.ml
@@ -98,6 +98,16 @@ and typlist p = function
   | Tcons(t, tl) ->
       fprintf p "@[<hov 2>(Tcons@ %a@ %a)@]" typ t typlist tl
 
+(* Access modes for members of structs or unions *)
+
+let bitfield p = function
+  | Full ->
+      fprintf p "Full"
+  | Bits(sz, sg, pos, width) ->
+      fprintf p "@[<hov 2>(Bits@ %a@ %a@ %a@ %a)@]"
+                intsize sz signedness sg
+                coqZ pos coqZ width
+
 (* Composite definitions *)
 
 let print_member p = function
@@ -119,4 +129,3 @@ let print_composite_definition p (Composite(id, su, m, a)) =
     (match su with Struct -> "Struct" | Union -> "Union")
     (print_list print_member) m
     attribute a
-
diff --git a/export/Clightgen.ml b/export/ExportDriver.ml
index 44c76cc6..d7980994 100644
--- a/export/Clightgen.ml
+++ b/export/ExportDriver.ml
@@ -22,15 +22,25 @@ open Driveraux
 open Frontend
 open Diagnostics
 
-let tool_name = "Clight generator"
+let tool_name = "CompCert AST generator"
 
-(* clightgen-specific options *)
+(* Specific options *)
 
+type export_mode = Mode_Csyntax | Mode_Clight
+let option_mode = ref Mode_Clight
 let option_normalize = ref false
 
-(* From CompCert C AST to Clight *)
+(* Export the CompCert Csyntax AST *)
 
-let compile_c_ast sourcename csyntax ofile =
+let export_csyntax sourcename csyntax ofile =
+  let oc = open_out ofile in
+  ExportCsyntax.print_program (Format.formatter_of_out_channel oc)
+                              csyntax sourcename;
+  close_out oc
+
+(* Transform the CompCert Csyntax AST into Clight and export it *)
+
+let export_clight sourcename csyntax ofile =
   let loc = file_loc sourcename in
   let clight =
     match SimplExpr.transl_program csyntax with
@@ -53,7 +63,7 @@ let compile_c_ast sourcename csyntax ofile =
                              clight sourcename !option_normalize;
   close_out oc
 
-(* From C source to Clight *)
+(* From C source to exported AST *)
 
 let compile_c_file sourcename ifile ofile =
   let set_dest dst opt ext =
@@ -62,7 +72,10 @@ let compile_c_file sourcename ifile ofile =
   set_dest Cprint.destination option_dparse ".parsed.c";
   set_dest PrintCsyntax.destination option_dcmedium ".compcert.c";
   set_dest PrintClight.destination option_dclight ".light.c";
-  compile_c_ast sourcename (parse_c_file sourcename ifile) ofile
+  let cs = parse_c_file sourcename ifile in
+  match !option_mode with
+  | Mode_Csyntax -> export_csyntax sourcename cs ofile
+  | Mode_Clight  -> export_clight sourcename cs ofile
 
 let output_filename sourcename suff =
   let prefixname = Filename.chop_suffix sourcename suff in
@@ -93,11 +106,13 @@ let process_i_file sourcename =
 
 let usage_string =
   version_string tool_name ^
-{|Usage: clightgen [options] <source files>
+{|Usage: clightgen <mode> [options] <source files>
 Recognized source files:
   .c             C source file
   .i or .p       C source file that should not be preprocessed
 Processing options:
+  -clight        Produce Clight AST  [default]
+  -csyntax       Produce Csyntax AST
   -normalize     Normalize the generated Clight code w.r.t. loads in expressions
   -canonical-idents  Use canonical numbers to represent identifiers  (default)
   -short-idents  Use small, non-canonical numbers to represent identifiers
@@ -143,7 +158,10 @@ let cmdline_actions =
   (* Getting version info *)
  @ version_options tool_name @
 (* Processing options *)
- [ Exact "-E", Set option_E;
+ [
+  Exact "-csyntax", Unit (fun () -> option_mode := Mode_Csyntax);
+  Exact "-clight", Unit (fun () -> option_mode := Mode_Clight);
+  Exact "-E", Set option_E;
   Exact "-normalize", Set option_normalize;
   Exact "-canonical-idents", Set Camlcoq.use_canonical_atoms;
   Exact "-short-idents", Unset Camlcoq.use_canonical_atoms;