Refactor clightgen

Split reusable parts of ExportClight.ml off, into
ExportBase.ml and ExportCtypes.ml.

Rename exportclight/ directory to export/

13 files changed, 644 insertions, 594 deletions

diff --git a/LICENSE b/LICENSE
index 6a4c62c3..54b36ed7 100644
--- a/LICENSE
+++ b/LICENSE
@@ -44,7 +44,7 @@ Foundation GNU Lesser General Public License, either version 2.1 or
 
   all files in the cparser/ directory
 
-  all files in the exportclight/ directory
+  all files in the export/ directory
 
   the Archi.v, Builtins1.v, CBuiltins.ml, and extractionMachdep.v files
   in directories aarch64, arm, powerpc, riscV, x86, x86_32, x86_64
diff --git a/Makefile b/Makefile
index a0f9fde6..c14f65c7 100644
--- a/Makefile
+++ b/Makefile
@@ -28,7 +28,7 @@ else
 ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
 endif
 
-DIRS := lib common $(ARCHDIRS) backend cfrontend driver exportclight cparser
+DIRS := lib common $(ARCHDIRS) backend cfrontend driver export cparser
 
 COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(d))
 
@@ -203,9 +203,9 @@ ccomp: .depend.extr compcert.ini driver/Version.ml FORCE
 ccomp.byte: .depend.extr compcert.ini driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr ccomp.byte
 
-clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE
+clightgen: .depend.extr compcert.ini export/Clightdefs.vo driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr clightgen
-clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE
+clightgen.byte: .depend.extr compcert.ini export/Clightdefs.vo driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr clightgen.byte
 
 runtime:
@@ -295,7 +295,7 @@ cparser/Parser.v: cparser/Parser.vy
 
 depend: $(GENERATED) depend1
 
-depend1: $(FILES) exportclight/Clightdefs.v
+depend1: $(FILES) export/Clightdefs.v
 	@echo "Analyzing Coq dependencies"
 	@$(COQDEP) $^ > .depend
 
diff --git a/Makefile.extr b/Makefile.extr
index fc631d78..e4b24ecd 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -45,7 +45,7 @@ cparser/pre_parser_messages.ml:
 
 DIRS=extraction \
   lib common $(ARCH) backend cfrontend cparser driver \
-  exportclight debug
+  export debug
 
 INCLUDES=$(patsubst %,-I %, $(DIRS))
 
@@ -112,7 +112,7 @@ ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)
 	@echo "Linking $@"
 	@$(OCAMLC) -o $@ $(LIBS_BYTE) $+
 
-CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx)
+CLIGHTGEN_OBJS:=$(shell $(MODORDER) export/Clightgen.cmx)
 
 ifeq ($(OCAML_NATIVE_COMP),true)
 clightgen: $(CLIGHTGEN_OBJS)
diff --git a/configure b/configure
index b342b143..10f60262 100755
--- a/configure
+++ b/configure
@@ -770,7 +770,7 @@ S backend
 S cfrontend
 S driver
 S debug
-S exportclight
+S export
 S cparser
 S extraction
 
@@ -781,7 +781,7 @@ B backend
 B cfrontend
 B driver
 B debug
-B exportclight
+B export
 B cparser
 B extraction
 EOF
diff --git a/exportclight/Clightdefs.v b/export/Clightdefs.v
index 708be1cb..708be1cb 100644
--- a/exportclight/Clightdefs.v
+++ b/export/Clightdefs.v
diff --git a/exportclight/Clightgen.ml b/export/Clightgen.ml
index 44c76cc6..44c76cc6 100644
--- a/exportclight/Clightgen.ml
+++ b/export/Clightgen.ml
diff --git a/exportclight/Clightnorm.ml b/export/Clightnorm.ml
index 88d44c08..88d44c08 100644
--- a/exportclight/Clightnorm.ml
+++ b/export/Clightnorm.ml
diff --git a/export/ExportBase.ml b/export/ExportBase.ml
new file mode 100644
index 00000000..b7d0170d
--- /dev/null
+++ b/export/ExportBase.ml
@@ -0,0 +1,261 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.                            *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Format
+open Camlcoq
+open AST
+
+(* Options, lists, pairs *)
+
+let print_option fn p = function
+  | None -> fprintf p "None"
+  | Some x -> fprintf p "(Some %a)" fn x
+
+let print_pair fn1 fn2 p (x1, x2) =
+  fprintf p "@[<hov 1>(%a,@ %a)@]" fn1 x1 fn2 x2
+
+let print_list fn p l =
+  match l with
+  | [] ->
+      fprintf p "nil"
+  | hd :: tl ->
+      fprintf p "@[<hov 1>(";
+      let rec plist = function
+      | [] -> fprintf p "nil"
+      | hd :: tl -> fprintf p "%a ::@ " fn hd; plist tl
+      in plist l;
+      fprintf p ")@]"
+
+(* Numbers *)
+
+let coqint p n =
+  let n = camlint_of_coqint n in
+  if n >= 0l
+  then fprintf p "(Int.repr %ld)" n
+  else fprintf p "(Int.repr (%ld))" n
+
+let coqptrofs p n =
+  let s = Z.to_string n in
+  if Z.ge n Z.zero
+  then fprintf p "(Ptrofs.repr %s)" s
+  else fprintf p "(Ptrofs.repr (%s))" s
+
+let coqint64 p n =
+  let n = camlint64_of_coqint n in
+  if n >= 0L
+  then fprintf p "(Int64.repr %Ld)" n
+  else fprintf p "(Int64.repr (%Ld))" n
+
+let coqfloat p n =
+  fprintf p "(Float.of_bits %a)" coqint64 (Floats.Float.to_bits n)
+
+let coqsingle p n =
+  fprintf p "(Float32.of_bits %a)" coqint (Floats.Float32.to_bits n)
+
+let positive p n =
+  fprintf p "%s%%positive" (Z.to_string (Z.Zpos n))
+
+let coqN p n =
+  fprintf p "%s%%N" (Z.to_string (Z.of_N n))
+
+let coqZ p n =
+  if Z.ge n Z.zero
+  then fprintf p "%s" (Z.to_string n)
+  else fprintf p "(%s)" (Z.to_string n)
+
+(* Coq strings *)
+
+let coqstring p s =
+  fprintf p "\"%s\"" (camlstring_of_coqstring s)
+
+(* Identifiers *)
+
+exception Not_an_identifier
+
+let sanitize_char = function
+  | 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' as c -> c
+  | ' ' | '$' -> '_'
+  | _ -> raise Not_an_identifier
+
+let sanitize s =
+  if s <> ""
+  then "_" ^ String.map sanitize_char s
+  else "empty_ident"
+
+let temp_names : (ident, string) Hashtbl.t = Hashtbl.create 17
+
+let ident p id =
+  try
+    let s = Hashtbl.find string_of_atom id in
+    fprintf p "%s" (sanitize s)
+  with Not_found | Not_an_identifier ->
+  try
+    let s = Hashtbl.find temp_names id in
+    fprintf p "%s" s
+  with Not_found ->
+    positive p id
+
+let iter_hashtbl_sorted (h: ('a, string) Hashtbl.t) (f: 'a * string -> unit) =
+  List.iter f
+    (List.fast_sort (fun (k1, d1) (k2, d2) -> String.compare d1 d2)
+      (Hashtbl.fold (fun k d accu -> (k, d) :: accu) h []))
+
+let define_idents p =
+  iter_hashtbl_sorted
+    string_of_atom
+    (fun (id, name) ->
+      try
+        if !use_canonical_atoms && id = pos_of_string name then
+          fprintf p "Definition %s : ident := $\"%s\".@ "
+                    (sanitize name) name
+        else
+          fprintf p "Definition %s : ident := %a.@ "
+                    (sanitize name) positive id
+      with Not_an_identifier ->
+        ());
+  iter_hashtbl_sorted
+    temp_names
+    (fun (id, name) ->
+      fprintf p "Definition %s : ident := %a.@ "
+                name positive id);
+  fprintf p "@ "
+
+let name_temporary t =
+  if not (Hashtbl.mem string_of_atom t) && not (Hashtbl.mem temp_names t)
+  then begin
+    let t0 = first_unused_ident () in
+    let d = Z.succ (Z.sub (Z.Zpos t) (Z.Zpos t0)) in
+    Hashtbl.add temp_names t ("_t'" ^ Z.to_string d)
+  end
+
+let name_opt_temporary = function
+  | None -> ()
+  | Some id -> name_temporary id
+
+(* External functions *)
+
+let asttype p t =
+  fprintf p "%s"
+     (match t with
+      | AST.Tint -> "AST.Tint"
+      | AST.Tfloat -> "AST.Tfloat"
+      | AST.Tlong -> "AST.Tlong"
+      | AST.Tsingle -> "AST.Tsingle"
+      | AST.Tany32 -> "AST.Tany32"
+      | AST.Tany64 -> "AST.Tany64")
+
+let astrettype p = function
+  | AST.Tret t -> asttype p t
+  | AST.Tvoid -> fprintf p "AST.Tvoid"
+  | AST.Tint8signed -> fprintf p "AST.Tint8signed"
+  | AST.Tint8unsigned -> fprintf p "AST.Tint8unsigned"
+  | AST.Tint16signed -> fprintf p "AST.Tint16signed"
+  | AST.Tint16unsigned -> fprintf p "AST.Tint16unsigned"
+
+let name_of_chunk = function
+  | Mint8signed -> "Mint8signed"
+  | Mint8unsigned -> "Mint8unsigned"
+  | Mint16signed -> "Mint16signed"
+  | Mint16unsigned -> "Mint16unsigned"
+  | Mint32 -> "Mint32"
+  | Mint64 -> "Mint64"
+  | Mfloat32 -> "Mfloat32"
+  | Mfloat64 -> "Mfloat64"
+  | Many32 -> "Many32"
+  | Many64 -> "Many64"
+
+let callconv p cc =
+  if cc = cc_default
+  then fprintf p "cc_default"
+  else fprintf p "{|cc_vararg:=%a; cc_unproto:=%b; cc_structret:=%b|}"
+                  (print_option coqZ) cc.cc_vararg cc.cc_unproto cc.cc_structret
+
+let signatur p sg =
+  fprintf p "@[<hov 2>(mksignature@ %a@ %a@ %a)@]"
+     (print_list asttype) sg.sig_args
+     astrettype sg.sig_res
+     callconv sg.sig_cc
+
+let external_function p = function
+  | EF_external(name, sg) ->
+      fprintf p "@[<hov 2>(EF_external %a@ %a)@]" coqstring name signatur sg
+  | EF_builtin(name, sg) ->
+      fprintf p "@[<hov 2>(EF_builtin %a@ %a)@]" coqstring name signatur sg
+  | EF_runtime(name, sg) ->
+      fprintf p "@[<hov 2>(EF_runtime %a@ %a)@]" coqstring name signatur sg
+  | EF_vload chunk ->
+      fprintf p "(EF_vload %s)" (name_of_chunk chunk)
+  | EF_vstore chunk ->
+      fprintf p "(EF_vstore %s)" (name_of_chunk chunk)
+  | EF_malloc -> fprintf p "EF_malloc"
+  | EF_free -> fprintf p "EF_free"
+  | EF_memcpy(sz, al) ->
+      fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al)
+  | EF_annot(kind, text, targs) ->
+      fprintf p "(EF_annot %a %a %a)"
+                positive kind coqstring text (print_list asttype) targs
+  | EF_annot_val(kind, text, targ) ->
+      fprintf p "(EF_annot_val %a %a %a)"
+                positive kind coqstring text asttype targ
+  | EF_debug(kind, text, targs) ->
+      fprintf p "(EF_debug %a %a %a)"
+                positive kind positive text (print_list asttype) targs
+  | EF_inline_asm(text, sg, clob) ->
+      fprintf p "@[<hov 2>(EF_inline_asm %a@ %a@ %a)@]"
+              coqstring text
+              signatur sg
+              (print_list coqstring) clob
+
+(* Variables *)
+
+let init_data p = function
+  | Init_int8 n -> fprintf p "Init_int8 %a" coqint n
+  | Init_int16 n -> fprintf p "Init_int16 %a" coqint n
+  | Init_int32 n -> fprintf p "Init_int32 %a" coqint n
+  | Init_int64 n -> fprintf p "Init_int64 %a" coqint64 n
+  | Init_float32 n -> fprintf p "Init_float32 %a" coqsingle n
+  | Init_float64 n -> fprintf p "Init_float64 %a" coqfloat n
+  | Init_space n -> fprintf p "Init_space %a" coqZ n
+  | Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqptrofs ofs
+
+let print_variable print_info p (id, v) =
+  fprintf p "Definition v%s := {|@ " (sanitize (extern_atom id));
+  fprintf p "  gvar_info := %a;@ " print_info v.gvar_info;
+  fprintf p "  gvar_init := %a;@ " (print_list init_data) v.gvar_init;
+  fprintf p "  gvar_readonly := %B;@ " v.gvar_readonly;
+  fprintf p "  gvar_volatile := %B@ " v.gvar_volatile;
+  fprintf p "|}.@ @ "
+
+(* Information about this run of clightgen *)
+
+let print_clightgen_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;
+  fprintf p "@ Definition build_tag := %S." Version.tag;
+  fprintf p "@ Definition build_branch := %S." Version.branch;
+  fprintf p "@ Definition arch := %S." Configuration.arch;
+  fprintf p "@ Definition model := %S." Configuration.model;
+  fprintf p "@ Definition abi := %S." Configuration.abi;
+  fprintf p "@ Definition bitsize := %d." (if Archi.ptr64 then 64 else 32);
+  fprintf p "@ Definition big_endian := %B." Archi.big_endian;
+  fprintf p "@ Definition source_file := %S." sourcefile;
+  begin match normalized with
+  | None -> ()
+  | Some b -> fprintf p "@ Definition normalized := %B." b
+  end;
+  fprintf p "@]@ End Info.@ @ "  
+  
diff --git a/export/ExportClight.ml b/export/ExportClight.ml
new file mode 100644
index 00000000..421db5ed
--- /dev/null
+++ b/export/ExportClight.ml
@@ -0,0 +1,251 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.                            *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Export Clight as a Coq file *)
+
+open Format
+open Camlcoq
+open AST
+open! Ctypes
+open Cop
+open Clight
+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 rec expr p = function
+  | Evar(id, t) ->
+      fprintf p "(Evar %a %a)" ident id typ t
+  | Etempvar(id, t) ->
+      fprintf p "(Etempvar %a %a)" ident id typ t
+  | Ederef(a1, t) ->
+      fprintf p "@[<hov 2>(Ederef@ %a@ %a)@]" expr a1 typ t
+  | Efield(a1, f, t) ->
+      fprintf p "@[<hov 2>(Efield@ %a@ %a@ %a)@]" expr a1 ident f typ t
+  | Econst_int(n, t) ->
+      fprintf p "(Econst_int %a %a)" coqint n typ t
+  | Econst_float(n, t) ->
+      fprintf p "(Econst_float %a %a)" coqfloat n typ t
+  | Econst_long(n, t) ->
+      fprintf p "(Econst_long %a %a)" coqint64 n typ t
+  | Econst_single(n, t) ->
+      fprintf p "(Econst_single %a %a)" coqsingle n typ t
+  | Eunop(op, a1, t) ->
+      fprintf p "@[<hov 2>(Eunop %s@ %a@ %a)@]"
+         (name_unop op) expr a1 typ t
+  | Eaddrof(a1, t) ->
+      fprintf p "@[<hov 2>(Eaddrof@ %a@ %a)@]" 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
+  | Esizeof(t1, t) ->
+      fprintf p "(Esizeof %a %a)" typ t1 typ t
+  | Ealignof(t1, t) ->
+      fprintf p "(Ealignof %a %a)" typ t1 typ t
+
+(* Statements *)
+
+let rec stmt p = function
+  | Sskip ->
+      fprintf p "Sskip"
+  | Sassign(e1, e2) ->
+      fprintf p "@[<hov 2>(Sassign@ %a@ %a)@]" expr e1 expr e2
+  | Sset(id, e2) ->
+      fprintf p "@[<hov 2>(Sset %a@ %a)@]" ident id expr e2
+  | Scall(optid, e1, el) ->
+      fprintf p "@[<hov 2>(Scall %a@ %a@ %a)@]"
+        (print_option ident) optid expr e1 (print_list expr) el
+  | Sbuiltin(optid, ef, tyl, el) ->
+      fprintf p "@[<hov 2>(Sbuiltin %a@ %a@ %a@ %a)@]"
+        (print_option ident) optid
+        external_function ef
+        typlist tyl
+        (print_list expr) el
+  | Ssequence(Sskip, s2) ->
+      stmt p s2
+  | Ssequence(s1, Sskip) ->
+      stmt p s1
+  | Ssequence(s1, s2) ->
+      fprintf p "@[<hv 2>(Ssequence@ %a@ %a)@]" stmt s1 stmt s2
+  | Sifthenelse(e, s1, s2) ->
+      fprintf p "@[<hv 2>(Sifthenelse %a@ %a@ %a)@]" expr e stmt s1 stmt s2
+  | Sloop (Ssequence (Sifthenelse(e, Sskip, Sbreak), s), Sskip) ->
+      fprintf p "@[<hv 2>(Swhile@ %a@ %a)@]" expr e stmt s
+  | Sloop (Ssequence (Ssequence(Sskip, Sifthenelse(e, Sskip, Sbreak)), s), Sskip) ->
+      fprintf p "@[<hv 2>(Swhile@ %a@ %a)@]" expr e stmt s
+  | Sloop(s1, s2) ->
+      fprintf p "@[<hv 2>(Sloop@ %a@ %a)@]" stmt s1 stmt s2
+  | Sbreak ->
+      fprintf p "Sbreak"
+  | Scontinue ->
+      fprintf p "Scontinue"
+  | Sswitch(e, cases) ->
+      fprintf p "@[<hv 2>(Sswitch %a@ %a)@]" expr e lblstmts cases
+  | Sreturn e ->
+      fprintf p "@[<hv 2>(Sreturn %a)@]" (print_option expr) e
+  | Slabel(lbl, s1) ->
+      fprintf p "@[<hv 2>(Slabel %a@ %a)@]" ident lbl stmt s1
+  | Sgoto lbl ->
+      fprintf p "(Sgoto %a)" ident lbl
+
+and lblstmts p = function
+  | LSnil ->
+      (fprintf p "LSnil")
+  | LScons(lbl, s, ls) ->
+      fprintf p "@[<hv 2>(LScons %a@ %a@ %a)@]"
+              (print_option coqZ) lbl stmt s lblstmts 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_temps := %a;@ " (print_list (print_pair ident typ)) f.fn_temps;
+  fprintf p "  fn_body :=@ ";
+  stmt 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 AST Ctypes Cop Clight Clightdefs.\n\
+Import Clightdefs.ClightNotations.\n\
+Local Open Scope Z_scope.\n\
+Local Open Scope string_scope.\n\
+Local Open Scope clight_scope.\n"
+
+(* Naming the compiler-generated temporaries occurring in the program *)
+
+let rec name_expr = function
+  | Evar(id, t) -> ()
+  | Etempvar(id, t) -> name_temporary id
+  | Ederef(a1, t) -> name_expr a1
+  | Efield(a1, f, t) -> name_expr a1
+  | Econst_int(n, t) -> ()
+  | Econst_float(n, t) -> ()
+  | Econst_long(n, t) -> ()
+  | Econst_single(n, t) -> ()
+  | Eunop(op, a1, t) -> name_expr a1
+  | Eaddrof(a1, t) -> name_expr a1
+  | Ebinop(op, a1, a2, t) -> name_expr a1; name_expr a2
+  | Ecast(a1, t) -> name_expr a1
+  | Esizeof(t1, t) -> ()
+  | Ealignof(t1, t) -> ()
+
+let rec name_stmt = function
+  | Sskip -> ()
+  | Sassign(e1, e2) -> name_expr e1; name_expr e2
+  | Sset(id, e2) -> name_temporary id; name_expr e2
+  | Scall(optid, e1, el) ->
+      name_opt_temporary optid; name_expr e1; List.iter name_expr el
+  | Sbuiltin(optid, ef, tyl, el) ->
+      name_opt_temporary optid; List.iter name_expr el
+  | Ssequence(s1, s2) -> name_stmt s1; name_stmt s2
+  | Sifthenelse(e, s1, s2) -> name_expr e; name_stmt s1; name_stmt s2
+  | Sloop(s1, s2) -> name_stmt s1; name_stmt s2
+  | Sbreak -> ()
+  | Scontinue -> ()
+  | Sswitch(e, cases) -> name_expr e; name_lblstmts cases
+  | Sreturn (Some e) -> name_expr e
+  | Sreturn None -> ()
+  | Slabel(lbl, s1) -> name_stmt s1
+  | Sgoto lbl -> ()
+
+and name_lblstmts = function
+  | LSnil -> ()
+  | LScons(lbl, s, ls) -> name_stmt s; name_lblstmts ls
+
+let name_function f =
+  List.iter (fun (id, ty) -> name_temporary id) f.fn_temps;
+  name_stmt f.fn_body
+
+let name_globdef (id, g) =
+  match g with
+  | Gfun(Ctypes.Internal f) -> name_function f
+  | _ -> ()
+
+let name_program p =
+  List.iter name_globdef p.Ctypes.prog_defs
+
+(* All together *)
+
+let print_program p prog sourcefile normalized =
+  Hashtbl.clear temp_names;
+  name_program prog;
+  fprintf p "@[<v 0>";
+  fprintf p "%s" prologue;
+  print_clightgen_info ~sourcefile ~normalized 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 : Clight.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
new file mode 100644
index 00000000..428a1459
--- /dev/null
+++ b/export/ExportCtypes.ml
@@ -0,0 +1,122 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.                            *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Format
+open Camlcoq
+open Ctypes
+open ExportBase
+
+(* Raw attributes *)
+
+let attribute p a =
+  if a = noattr then
+    fprintf p "noattr"
+  else
+    fprintf p "{| attr_volatile := %B; attr_alignas := %a |}"
+              a.attr_volatile
+              (print_option coqN) a.attr_alignas
+
+(* Raw int size and signedness *)
+
+let intsize p sz =
+  fprintf p "%s"
+    (match sz with 
+     | I8 -> "I8"
+     | I16 -> "I16"
+     | I32 -> "I32"
+     | IBool -> "IBool")
+
+let signedness p sg =
+  fprintf p "%s"
+    (match sg with
+      | Signed -> "Signed"
+      | Unsigned -> "Unsigned")
+
+(* Types *)
+
+let rec typ p t =
+  match attr_of_type t with
+  | { attr_volatile = false; attr_alignas = None} ->
+        rtyp p t
+  | { attr_volatile = true; attr_alignas = None} ->
+        fprintf p "(tvolatile %a)" rtyp t
+  | { attr_volatile = false; attr_alignas = Some n} ->
+        fprintf p "(talignas %a %a)" coqN n rtyp t
+  | { attr_volatile = true; attr_alignas = Some n} ->
+        fprintf p "(tvolatile_alignas %a %a)" coqN n rtyp t
+
+and rtyp p = function
+  | Tvoid -> fprintf p "tvoid"
+  | Ctypes.Tint(sz, sg, _) ->
+      fprintf p "%s" (
+        match sz, sg with
+        | I8, Signed -> "tschar"
+        | I8, Unsigned -> "tuchar"
+        | I16, Signed -> "tshort"
+        | I16, Unsigned -> "tushort"
+        | I32, Signed -> "tint"
+        | I32, Unsigned -> "tuint"
+        | IBool, _ -> "tbool")
+  | Ctypes.Tlong(sg, _) ->
+      fprintf p "%s" (
+        match sg with
+        | Signed -> "tlong"
+        | Unsigned -> "tulong")
+  | Ctypes.Tfloat(sz, _) ->
+      fprintf p "%s" (
+        match sz with
+        | F32 -> "tfloat"
+        | F64 -> "tdouble")
+  | Tpointer(t, _) ->
+      fprintf p "(tptr %a)" typ t
+  | Tarray(t, sz, _) ->
+      fprintf p "(tarray %a %ld)" typ t (Z.to_int32 sz)
+  | Tfunction(targs, tres, cc) ->
+      fprintf p "@[<hov 2>(Tfunction@ %a@ %a@ %a)@]"
+                typlist targs typ tres callconv cc
+  | Tstruct(id, _) ->
+      fprintf p "(Tstruct %a noattr)" ident id
+  | Tunion(id, _) ->
+      fprintf p "(Tunion %a noattr)" ident id
+
+and typlist p = function
+  | Tnil ->
+      fprintf p "Tnil"
+  | Tcons(t, tl) ->
+      fprintf p "@[<hov 2>(Tcons@ %a@ %a)@]" typ t typlist tl
+
+(* Composite definitions *)
+
+let print_member p = function
+  | Member_plain (id, ty) ->
+      fprintf p "@[<hov 2>Member_plain@ %a@ %a@]"
+              ident id typ ty
+  | Member_bitfield (id, sz, sg, a, width, pad) ->
+      fprintf p "@[<hov 2>Member_bitfield@ %a@ %a@ %a@ %a@ %a@ %B@]"
+              ident id
+              intsize sz
+              signedness sg
+              attribute a
+              coqZ width
+              pad
+
+let print_composite_definition p (Composite(id, su, m, a)) =
+  fprintf p "@[<hv 2>Composite %a %s@ %a@ %a@]"
+    ident id
+    (match su with Struct -> "Struct" | Union -> "Union")
+    (print_list print_member) m
+    attribute a
+
diff --git a/exportclight/README.md b/export/README.md
index 85e0790b..85e0790b 100644
--- a/exportclight/README.md
+++ b/export/README.md
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
deleted file mode 100644
index 742b3a5c..00000000
--- a/exportclight/ExportClight.ml
+++ /dev/null
@@ -1,584 +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 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.                            *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Export Clight as a Coq file *)
-
-open Format
-open Camlcoq
-open AST
-open! Ctypes
-open Cop
-open Clight
-
-(* Options, lists, pairs *)
-
-let print_option fn p = function
-  | None -> fprintf p "None"
-  | Some x -> fprintf p "(Some %a)" fn x
-
-let print_pair fn1 fn2 p (x1, x2) =
-  fprintf p "@[<hov 1>(%a,@ %a)@]" fn1 x1 fn2 x2
-
-let print_list fn p l =
-  match l with
-  | [] ->
-      fprintf p "nil"
-  | hd :: tl ->
-      fprintf p "@[<hov 1>(";
-      let rec plist = function
-      | [] -> fprintf p "nil"
-      | hd :: tl -> fprintf p "%a ::@ " fn hd; plist tl
-      in plist l;
-      fprintf p ")@]"
-
-(* Numbers *)
-
-let coqint p n =
-  let n = camlint_of_coqint n in
-  if n >= 0l
-  then fprintf p "(Int.repr %ld)" n
-  else fprintf p "(Int.repr (%ld))" n
-
-let coqptrofs p n =
-  let s = Z.to_string n in
-  if Z.ge n Z.zero
-  then fprintf p "(Ptrofs.repr %s)" s
-  else fprintf p "(Ptrofs.repr (%s))" s
-
-let coqint64 p n =
-  let n = camlint64_of_coqint n in
-  if n >= 0L
-  then fprintf p "(Int64.repr %Ld)" n
-  else fprintf p "(Int64.repr (%Ld))" n
-
-let coqfloat p n =
-  fprintf p "(Float.of_bits %a)" coqint64 (Floats.Float.to_bits n)
-
-let coqsingle p n =
-  fprintf p "(Float32.of_bits %a)" coqint (Floats.Float32.to_bits n)
-
-let positive p n =
-  fprintf p "%s%%positive" (Z.to_string (Z.Zpos n))
-
-let coqN p n =
-  fprintf p "%s%%N" (Z.to_string (Z.of_N n))
-
-let coqZ p n =
-  if Z.ge n Z.zero
-  then fprintf p "%s" (Z.to_string n)
-  else fprintf p "(%s)" (Z.to_string n)
-
-(* Coq strings *)
-
-let coqstring p s =
-  fprintf p "\"%s\"" (camlstring_of_coqstring s)
-
-(* Identifiers *)
-
-exception Not_an_identifier
-
-let sanitize_char = function
-  | 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' as c -> c
-  | ' ' | '$' -> '_'
-  | _ -> raise Not_an_identifier
-
-let sanitize s =
-  if s <> ""
-  then "_" ^ String.map sanitize_char s
-  else "empty_ident"
-
-let temp_names : (ident, string) Hashtbl.t = Hashtbl.create 17
-
-let ident p id =
-  try
-    let s = Hashtbl.find string_of_atom id in
-    fprintf p "%s" (sanitize s)
-  with Not_found | Not_an_identifier ->
-  try
-    let s = Hashtbl.find temp_names id in
-    fprintf p "%s" s
-  with Not_found ->
-    positive p id
-
-let iter_hashtbl_sorted (h: ('a, string) Hashtbl.t) (f: 'a * string -> unit) =
-  List.iter f
-    (List.fast_sort (fun (k1, d1) (k2, d2) -> String.compare d1 d2)
-      (Hashtbl.fold (fun k d accu -> (k, d) :: accu) h []))
-
-let define_idents p =
-  iter_hashtbl_sorted
-    string_of_atom
-    (fun (id, name) ->
-      try
-        if !use_canonical_atoms && id = pos_of_string name then
-          fprintf p "Definition %s : ident := $\"%s\".@ "
-                    (sanitize name) name
-        else
-          fprintf p "Definition %s : ident := %a.@ "
-                    (sanitize name) positive id
-      with Not_an_identifier ->
-        ());
-  iter_hashtbl_sorted
-    temp_names
-    (fun (id, name) ->
-      fprintf p "Definition %s : ident := %a.@ "
-                name positive id);
-  fprintf p "@ "
-
-let name_temporary t =
-  if not (Hashtbl.mem string_of_atom t) && not (Hashtbl.mem temp_names t)
-  then begin
-    let t0 = first_unused_ident () in
-    let d = Z.succ (Z.sub (Z.Zpos t) (Z.Zpos t0)) in
-    Hashtbl.add temp_names t ("_t'" ^ Z.to_string d)
-  end
-
-let name_opt_temporary = function
-  | None -> ()
-  | Some id -> name_temporary id
-
-(* Raw attributes *)
-
-let attribute p a =
-  if a = noattr then
-    fprintf p "noattr"
-  else
-    fprintf p "{| attr_volatile := %B; attr_alignas := %a |}"
-              a.attr_volatile
-              (print_option coqN) a.attr_alignas
-
-(* Raw int size and signedness *)
-
-let intsize p sz =
-  fprintf p "%s"
-    (match sz with 
-     | I8 -> "I8"
-     | I16 -> "I16"
-     | I32 -> "I32"
-     | IBool -> "IBool")
-
-let signedness p sg =
-  fprintf p "%s"
-    (match sg with
-      | Signed -> "Signed"
-      | Unsigned -> "Unsigned")
-
-(* Types *)
-
-let rec typ p t =
-  match attr_of_type t with
-  | { attr_volatile = false; attr_alignas = None} ->
-        rtyp p t
-  | { attr_volatile = true; attr_alignas = None} ->
-        fprintf p "(tvolatile %a)" rtyp t
-  | { attr_volatile = false; attr_alignas = Some n} ->
-        fprintf p "(talignas %a %a)" coqN n rtyp t
-  | { attr_volatile = true; attr_alignas = Some n} ->
-        fprintf p "(tvolatile_alignas %a %a)" coqN n rtyp t
-
-and rtyp p = function
-  | Tvoid -> fprintf p "tvoid"
-  | Ctypes.Tint(sz, sg, _) ->
-      fprintf p "%s" (
-        match sz, sg with
-        | I8, Signed -> "tschar"
-        | I8, Unsigned -> "tuchar"
-        | I16, Signed -> "tshort"
-        | I16, Unsigned -> "tushort"
-        | I32, Signed -> "tint"
-        | I32, Unsigned -> "tuint"
-        | IBool, _ -> "tbool")
-  | Ctypes.Tlong(sg, _) ->
-      fprintf p "%s" (
-        match sg with
-        | Signed -> "tlong"
-        | Unsigned -> "tulong")
-  | Ctypes.Tfloat(sz, _) ->
-      fprintf p "%s" (
-        match sz with
-        | F32 -> "tfloat"
-        | F64 -> "tdouble")
-  | Tpointer(t, _) ->
-      fprintf p "(tptr %a)" typ t
-  | Tarray(t, sz, _) ->
-      fprintf p "(tarray %a %ld)" typ t (Z.to_int32 sz)
-  | Tfunction(targs, tres, cc) ->
-      fprintf p "@[<hov 2>(Tfunction@ %a@ %a@ %a)@]"
-                typlist targs typ tres callconv cc
-  | Tstruct(id, _) ->
-      fprintf p "(Tstruct %a noattr)" ident id
-  | Tunion(id, _) ->
-      fprintf p "(Tunion %a noattr)" ident id
-
-and typlist p = function
-  | Tnil ->
-      fprintf p "Tnil"
-  | Tcons(t, tl) ->
-      fprintf p "@[<hov 2>(Tcons@ %a@ %a)@]" typ t typlist tl
-
-and callconv p cc =
-  if cc = cc_default
-  then fprintf p "cc_default"
-  else fprintf p "{|cc_vararg:=%a; cc_unproto:=%b; cc_structret:=%b|}"
-                  (print_option coqZ) cc.cc_vararg cc.cc_unproto cc.cc_structret
-
-(* External functions *)
-
-let asttype p t =
-  fprintf p "%s"
-     (match t with
-      | AST.Tint -> "AST.Tint"
-      | AST.Tfloat -> "AST.Tfloat"
-      | AST.Tlong -> "AST.Tlong"
-      | AST.Tsingle -> "AST.Tsingle"
-      | AST.Tany32 -> "AST.Tany32"
-      | AST.Tany64 -> "AST.Tany64")
-
-let astrettype p = function
-  | AST.Tret t -> asttype p t
-  | AST.Tvoid -> fprintf p "AST.Tvoid"
-  | AST.Tint8signed -> fprintf p "AST.Tint8signed"
-  | AST.Tint8unsigned -> fprintf p "AST.Tint8unsigned"
-  | AST.Tint16signed -> fprintf p "AST.Tint16signed"
-  | AST.Tint16unsigned -> fprintf p "AST.Tint16unsigned"
-
-let name_of_chunk = function
-  | Mint8signed -> "Mint8signed"
-  | Mint8unsigned -> "Mint8unsigned"
-  | Mint16signed -> "Mint16signed"
-  | Mint16unsigned -> "Mint16unsigned"
-  | Mint32 -> "Mint32"
-  | Mint64 -> "Mint64"
-  | Mfloat32 -> "Mfloat32"
-  | Mfloat64 -> "Mfloat64"
-  | Many32 -> "Many32"
-  | Many64 -> "Many64"
-
-let signatur p sg =
-  fprintf p "@[<hov 2>(mksignature@ %a@ %a@ %a)@]"
-     (print_list asttype) sg.sig_args
-     astrettype sg.sig_res
-     callconv sg.sig_cc
-
-let external_function p = function
-  | EF_external(name, sg) ->
-      fprintf p "@[<hov 2>(EF_external %a@ %a)@]" coqstring name signatur sg
-  | EF_builtin(name, sg) ->
-      fprintf p "@[<hov 2>(EF_builtin %a@ %a)@]" coqstring name signatur sg
-  | EF_runtime(name, sg) ->
-      fprintf p "@[<hov 2>(EF_runtime %a@ %a)@]" coqstring name signatur sg
-  | EF_vload chunk ->
-      fprintf p "(EF_vload %s)" (name_of_chunk chunk)
-  | EF_vstore chunk ->
-      fprintf p "(EF_vstore %s)" (name_of_chunk chunk)
-  | EF_malloc -> fprintf p "EF_malloc"
-  | EF_free -> fprintf p "EF_free"
-  | EF_memcpy(sz, al) ->
-      fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al)
-  | EF_annot(kind, text, targs) ->
-      fprintf p "(EF_annot %a %a %a)"
-                positive kind coqstring text (print_list asttype) targs
-  | EF_annot_val(kind, text, targ) ->
-      fprintf p "(EF_annot_val %a %a %a)"
-                positive kind coqstring text asttype targ
-  | EF_debug(kind, text, targs) ->
-      fprintf p "(EF_debug %a %a %a)"
-                positive kind positive text (print_list asttype) targs
-  | EF_inline_asm(text, sg, clob) ->
-      fprintf p "@[<hov 2>(EF_inline_asm %a@ %a@ %a)@]"
-              coqstring text
-              signatur sg
-              (print_list coqstring) clob
-
-(* 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 rec expr p = function
-  | Evar(id, t) ->
-      fprintf p "(Evar %a %a)" ident id typ t
-  | Etempvar(id, t) ->
-      fprintf p "(Etempvar %a %a)" ident id typ t
-  | Ederef(a1, t) ->
-      fprintf p "@[<hov 2>(Ederef@ %a@ %a)@]" expr a1 typ t
-  | Efield(a1, f, t) ->
-      fprintf p "@[<hov 2>(Efield@ %a@ %a@ %a)@]" expr a1 ident f typ t
-  | Econst_int(n, t) ->
-      fprintf p "(Econst_int %a %a)" coqint n typ t
-  | Econst_float(n, t) ->
-      fprintf p "(Econst_float %a %a)" coqfloat n typ t
-  | Econst_long(n, t) ->
-      fprintf p "(Econst_long %a %a)" coqint64 n typ t
-  | Econst_single(n, t) ->
-      fprintf p "(Econst_single %a %a)" coqsingle n typ t
-  | Eunop(op, a1, t) ->
-      fprintf p "@[<hov 2>(Eunop %s@ %a@ %a)@]"
-         (name_unop op) expr a1 typ t
-  | Eaddrof(a1, t) ->
-      fprintf p "@[<hov 2>(Eaddrof@ %a@ %a)@]" 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
-  | Esizeof(t1, t) ->
-      fprintf p "(Esizeof %a %a)" typ t1 typ t
-  | Ealignof(t1, t) ->
-      fprintf p "(Ealignof %a %a)" typ t1 typ t
-
-(* Statements *)
-
-let rec stmt p = function
-  | Sskip ->
-      fprintf p "Sskip"
-  | Sassign(e1, e2) ->
-      fprintf p "@[<hov 2>(Sassign@ %a@ %a)@]" expr e1 expr e2
-  | Sset(id, e2) ->
-      fprintf p "@[<hov 2>(Sset %a@ %a)@]" ident id expr e2
-  | Scall(optid, e1, el) ->
-      fprintf p "@[<hov 2>(Scall %a@ %a@ %a)@]"
-        (print_option ident) optid expr e1 (print_list expr) el
-  | Sbuiltin(optid, ef, tyl, el) ->
-      fprintf p "@[<hov 2>(Sbuiltin %a@ %a@ %a@ %a)@]"
-        (print_option ident) optid
-        external_function ef
-        typlist tyl
-        (print_list expr) el
-  | Ssequence(Sskip, s2) ->
-      stmt p s2
-  | Ssequence(s1, Sskip) ->
-      stmt p s1
-  | Ssequence(s1, s2) ->
-      fprintf p "@[<hv 2>(Ssequence@ %a@ %a)@]" stmt s1 stmt s2
-  | Sifthenelse(e, s1, s2) ->
-      fprintf p "@[<hv 2>(Sifthenelse %a@ %a@ %a)@]" expr e stmt s1 stmt s2
-  | Sloop (Ssequence (Sifthenelse(e, Sskip, Sbreak), s), Sskip) ->
-      fprintf p "@[<hv 2>(Swhile@ %a@ %a)@]" expr e stmt s
-  | Sloop (Ssequence (Ssequence(Sskip, Sifthenelse(e, Sskip, Sbreak)), s), Sskip) ->
-      fprintf p "@[<hv 2>(Swhile@ %a@ %a)@]" expr e stmt s
-  | Sloop(s1, s2) ->
-      fprintf p "@[<hv 2>(Sloop@ %a@ %a)@]" stmt s1 stmt s2
-  | Sbreak ->
-      fprintf p "Sbreak"
-  | Scontinue ->
-      fprintf p "Scontinue"
-  | Sswitch(e, cases) ->
-      fprintf p "@[<hv 2>(Sswitch %a@ %a)@]" expr e lblstmts cases
-  | Sreturn e ->
-      fprintf p "@[<hv 2>(Sreturn %a)@]" (print_option expr) e
-  | Slabel(lbl, s1) ->
-      fprintf p "@[<hv 2>(Slabel %a@ %a)@]" ident lbl stmt s1
-  | Sgoto lbl ->
-      fprintf p "(Sgoto %a)" ident lbl
-
-and lblstmts p = function
-  | LSnil ->
-      (fprintf p "LSnil")
-  | LScons(lbl, s, ls) ->
-      fprintf p "@[<hv 2>(LScons %a@ %a@ %a)@]"
-              (print_option coqZ) lbl stmt s lblstmts ls
-
-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_temps := %a;@ " (print_list (print_pair ident typ)) f.fn_temps;
-  fprintf p "  fn_body :=@ ";
-  stmt p f.fn_body;
-  fprintf p "@ |}.@ @ "
-
-let init_data p = function
-  | Init_int8 n -> fprintf p "Init_int8 %a" coqint n
-  | Init_int16 n -> fprintf p "Init_int16 %a" coqint n
-  | Init_int32 n -> fprintf p "Init_int32 %a" coqint n
-  | Init_int64 n -> fprintf p "Init_int64 %a" coqint64 n
-  | Init_float32 n -> fprintf p "Init_float32 %a" coqsingle n
-  | Init_float64 n -> fprintf p "Init_float64 %a" coqfloat n
-  | Init_space n -> fprintf p "Init_space %a" coqZ n
-  | Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqptrofs ofs
-
-let print_variable p (id, v) =
-  fprintf p "Definition v%s := {|@ " (sanitize (extern_atom id));
-  fprintf p "  gvar_info := %a;@ " typ v.gvar_info;
-  fprintf p "  gvar_init := %a;@ " (print_list init_data) v.gvar_init;
-  fprintf p "  gvar_readonly := %B;@ " v.gvar_readonly;
-  fprintf p "  gvar_volatile := %B@ " v.gvar_volatile;
-  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 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))
-
-(* Composite definitions *)
-
-let print_member p = function
-  | Member_plain (id, ty) ->
-      fprintf p "@[<hov 2>Member_plain@ %a@ %a@]"
-              ident id typ ty
-  | Member_bitfield (id, sz, sg, a, width, pad) ->
-      fprintf p "@[<hov 2>Member_bitfield@ %a@ %a@ %a@ %a@ %a@ %B@]"
-              ident id
-              intsize sz
-              signedness sg
-              attribute a
-              coqZ width
-              pad
-
-let print_composite_definition p (Composite(id, su, m, a)) =
-  fprintf p "@[<hv 2>Composite %a %s@ %a@ %a@]"
-    ident id
-    (match su with Struct -> "Struct" | Union -> "Union")
-    (print_list print_member) m
-    attribute a
-
-(* The prologue *)
-
-let prologue = "\
-From Coq Require Import String List ZArith.\n\
-From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\
-Import Clightdefs.ClightNotations.\n\
-Local Open Scope Z_scope.\n\
-Local Open Scope string_scope.\n\
-Local Open Scope clight_scope.\n"
-
-(* Naming the compiler-generated temporaries occurring in the program *)
-
-let rec name_expr = function
-  | Evar(id, t) -> ()
-  | Etempvar(id, t) -> name_temporary id
-  | Ederef(a1, t) -> name_expr a1
-  | Efield(a1, f, t) -> name_expr a1
-  | Econst_int(n, t) -> ()
-  | Econst_float(n, t) -> ()
-  | Econst_long(n, t) -> ()
-  | Econst_single(n, t) -> ()
-  | Eunop(op, a1, t) -> name_expr a1
-  | Eaddrof(a1, t) -> name_expr a1
-  | Ebinop(op, a1, a2, t) -> name_expr a1; name_expr a2
-  | Ecast(a1, t) -> name_expr a1
-  | Esizeof(t1, t) -> ()
-  | Ealignof(t1, t) -> ()
-
-let rec name_stmt = function
-  | Sskip -> ()
-  | Sassign(e1, e2) -> name_expr e1; name_expr e2
-  | Sset(id, e2) -> name_temporary id; name_expr e2
-  | Scall(optid, e1, el) ->
-      name_opt_temporary optid; name_expr e1; List.iter name_expr el
-  | Sbuiltin(optid, ef, tyl, el) ->
-      name_opt_temporary optid; List.iter name_expr el
-  | Ssequence(s1, s2) -> name_stmt s1; name_stmt s2
-  | Sifthenelse(e, s1, s2) -> name_expr e; name_stmt s1; name_stmt s2
-  | Sloop(s1, s2) -> name_stmt s1; name_stmt s2
-  | Sbreak -> ()
-  | Scontinue -> ()
-  | Sswitch(e, cases) -> name_expr e; name_lblstmts cases
-  | Sreturn (Some e) -> name_expr e
-  | Sreturn None -> ()
-  | Slabel(lbl, s1) -> name_stmt s1
-  | Sgoto lbl -> ()
-
-and name_lblstmts = function
-  | LSnil -> ()
-  | LScons(lbl, s, ls) -> name_stmt s; name_lblstmts ls
-
-let name_function f =
-  List.iter (fun (id, ty) -> name_temporary id) f.fn_temps;
-  name_stmt f.fn_body
-
-let name_globdef (id, g) =
-  match g with
-  | Gfun(Ctypes.Internal f) -> name_function f
-  | _ -> ()
-
-let name_program p =
-  List.iter name_globdef p.Ctypes.prog_defs
-
-(* Information about this run of clightgen *)
-
-let print_clightgen_info p sourcefile normalized =
-  fprintf p "@[<v 2>Module Info.";
-  fprintf p "@ Definition version := %S." Version.version;
-  fprintf p "@ Definition build_number := %S." Version.buildnr;
-  fprintf p "@ Definition build_tag := %S." Version.tag;
-  fprintf p "@ Definition build_branch := %S." Version.branch;
-  fprintf p "@ Definition arch := %S." Configuration.arch;
-  fprintf p "@ Definition model := %S." Configuration.model;
-  fprintf p "@ Definition abi := %S." Configuration.abi;
-  fprintf p "@ Definition bitsize := %d." (if Archi.ptr64 then 64 else 32);
-  fprintf p "@ Definition big_endian := %B." Archi.big_endian;
-  fprintf p "@ Definition source_file := %S." sourcefile;
-  fprintf p "@ Definition normalized := %B." normalized;
-  fprintf p "@]@ End Info.@ @ "  
-  
-(* All together *)
-
-let print_program p prog sourcefile normalized =
-  Hashtbl.clear temp_names;
-  name_program prog;
-  fprintf p "@[<v 0>";
-  fprintf p "%s" prologue;
-  print_clightgen_info p sourcefile normalized;
-  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 : Clight.program := @ ";
-  fprintf p "  mkprogram composites global_definitions public_idents %a Logic.I.@ @ "
-            ident prog.Ctypes.prog_main;
-  fprintf p "@]@."
diff --git a/test/clightgen/Makefile b/test/clightgen/Makefile
index f0e9d961..83ba0fd3 100644
--- a/test/clightgen/Makefile
+++ b/test/clightgen/Makefile
@@ -5,7 +5,7 @@ ARCHDIRS=$(ARCH)
 else
 ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
 endif
-RECDIRS := lib common $(ARCHDIRS) cfrontend  exportclight
+RECDIRS := lib common $(ARCHDIRS) cfrontend export
 COQINCLUDES := $(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d))
 ifeq ($(LIBRARY_FLOCQ),local)
 COQINCLUDES += -R ../../flocq Flocq