Merge branch 'master' into dwarf

33 files changed, 1612 insertions, 606 deletions

diff --git a/.gitignore b/.gitignore
index 72fb793b..36372810 100644
--- a/.gitignore
+++ b/.gitignore
@@ -39,6 +39,7 @@ cparser/Parser.v
 cparser/Lexer.ml
 cparser/pre_parser.ml
 cparser/pre_parser.mli
+lib/Readconfig.ml
 lib/Tokenize.ml
 # Documentation
 doc/coq2html
diff --git a/Makefile b/Makefile
index 99fd7223..157fb1a2 100644
--- a/Makefile
+++ b/Makefile
@@ -174,15 +174,15 @@ doc/coq2html.ml: doc/coq2html.mll
 	ocamllex -q doc/coq2html.mll
 
 tools/ndfun: tools/ndfun.ml
-	ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml $(LINKERSPEC)
+	ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml
 tools/modorder: tools/modorder.ml
-	ocamlopt -o tools/modorder str.cmxa tools/modorder.ml $(LINKERSPEC)
+	ocamlopt -o tools/modorder str.cmxa tools/modorder.ml
 
 latexdoc:
 	cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES)
 
 %.vo: %.v
-	@rm -f doc/glob/$(*F).glob
+	@rm -f doc/$(*F).glob
 	@echo "COQC $*.v"
 	@$(COQC) -dump-glob doc/$(*F).glob $*.v
 
diff --git a/Makefile.extr b/Makefile.extr
index f5f7e7b4..4e17e904 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -61,7 +61,7 @@ endif
 
 OCAMLC=ocamlc$(DOTOPT) $(COMPFLAGS)
 OCAMLOPT=ocamlopt$(DOTOPT) $(COMPFLAGS)
-OCAMLDEP=ocamldep$(DOTOPT) $(INCLUDES)
+OCAMLDEP=ocamldep$(DOTOPT) -slash $(INCLUDES)
 
 # Compilers used for Camlp4-preprocessed code.  Note that we cannot
 # use the .opt compilers (because ocamlfind doesn't support them).
@@ -75,9 +75,11 @@ OCAMLLEX=ocamllex -q
 MODORDER=tools/modorder .depend.extr
 
 PARSERS=backend/CMparser.mly cparser/pre_parser.mly
-LEXERS=backend/CMlexer.mll cparser/Lexer.mll lib/Tokenize.mll
+LEXERS=backend/CMlexer.mll cparser/Lexer.mll \
+       lib/Tokenize.mll lib/Readconfig.mll
 
-LIBS=str.cmxa
+LIBS=str.cmxa unix.cmxa
+CHECKLINK_LIBS=str.cmxa
 
 EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte
 GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml)
@@ -90,11 +92,11 @@ CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx)
 
 ccomp: $(CCOMP_OBJS)
 	@echo "Linking $@"
-	@$(OCAMLOPT) -o $@ $(LIBS) $+ $(LINKERSPEC)
+	@$(OCAMLOPT) -o $@ $(LIBS) $+
 
 ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)
 	@echo "Linking $@"
-	@$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ $(LINKERSPEC)
+	@$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+
 
 ifeq ($(CCHECKLINK),true)
 
@@ -102,11 +104,11 @@ CCHECKLINK_OBJS:=$(shell $(MODORDER) checklink/Validator.cmx)
 
 cchecklink: $(CCHECKLINK_OBJS)
 	@echo "Linking $@"
-	@$(OCAMLOPT_P4) -linkpkg -o $@ $(LIBS) $+
+	@$(OCAMLOPT_P4) -linkpkg -o $@ $(CHECKLINK_LIBS) $+
 
 cchecklink.byte: $(CCHECKLINK_OBJS:.cmx=.cmo)
 	@echo "Linking $@"
-	@$(OCAMLC_P4) -linkpkg -o $@ $(LIBS:.cmxa=.cma) $+
+	@$(OCAMLC_P4) -linkpkg -o $@ $(CHECKLINK_LIBS:.cmxa=.cma) $+
 
 endif
 
@@ -156,17 +158,14 @@ clean:
 	rm -f $(GENERATED)
 	for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done
 
-cleansource:
-	rm -f $(EXECUTABLES)
-	for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done
-
 # Generation of .depend.extr
 
 depend: $(GENERATED)
 	@echo "Analyzing OCaml dependencies"
-	@for d in $(DIRS); do $(OCAMLDEP) $$d/*.mli $$d/*.ml; done > .depend.extr
+	@$(OCAMLDEP) $(foreach d,$(DIRS),$(wildcard $(d)/*.mli $(d)/*.ml)) >.depend.extr
+	@$(OCAMLDEP) $(GENERATED) >> .depend.extr
 ifneq ($(strip $(DIRS_P4)),)
-	@for d in $(DIRS_P4); do $(OCAMLDEP_P4) $$d/*.mli $$d/*.ml; done >> .depend.extr
+	@$(OCAMLDEP_P4) $(foreach d,$(DIRS_P4),$(wildcard $(d)/*.mli $(d)/*.ml)) >>.depend.extr
 endif
 
 
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 952d148d..ed67286f 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -12,6 +12,7 @@
 
 (** Animating the CompCert C semantics *)
 
+Require Import String.
 Require Import Axioms.
 Require Import Classical.
 Require Import Coqlib.
@@ -31,6 +32,9 @@ Require Import Csyntax.
 Require Import Csem.
 Require Cstrategy.
 
+Local Open Scope string_scope.
+Local Open Scope list_scope.
+
 (** Error monad with options or lists *)
 
 Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end)
@@ -661,9 +665,9 @@ Qed.
 (** * Reduction of expressions *)
 
 Inductive reduction: Type :=
-  | Lred (l': expr) (m': mem)
-  | Rred (r': expr) (m': mem) (t: trace)
-  | Callred (fd: fundef) (args: list val) (tyres: type) (m': mem)
+  | Lred (rule: string) (l': expr) (m': mem)
+  | Rred (rule: string) (r': expr) (m': mem) (t: trace)
+  | Callred (rule: string) (fd: fundef) (args: list val) (tyres: type) (m': mem)
   | Stuckred.
 
 Section EXPRS.
@@ -728,15 +732,15 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match e!x with
       | Some(b, ty') =>
           check type_eq ty ty';
-          topred (Lred (Eloc b Int.zero ty) m)
+          topred (Lred "red_var_local" (Eloc b Int.zero ty) m)
       | None =>
           do b <- Genv.find_symbol ge x;
-          topred (Lred (Eloc b Int.zero ty) m)
+          topred (Lred "red_var_global" (Eloc b Int.zero ty) m)
       end
   | LV, Ederef r ty =>
       match is_val r with
       | Some(Vptr b ofs, ty') =>
-          topred (Lred (Eloc b ofs ty) m)
+          topred (Lred "red_deref" (Eloc b ofs ty) m)
       | Some _ =>
           stuck
       | None =>
@@ -750,11 +754,11 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
               do co <- ge.(genv_cenv)!id;
               match field_offset ge f (co_members co) with
               | Error _ => stuck
-              | OK delta => topred (Lred (Eloc b (Int.add ofs (Int.repr delta)) ty) m)
+              | OK delta => topred (Lred "red_field_struct" (Eloc b (Int.add ofs (Int.repr delta)) ty) m)
               end
           | Tunion id _ =>
               do co <- ge.(genv_cenv)!id;
-              topred (Lred (Eloc b ofs ty) m)
+              topred (Lred "red_field_union" (Eloc b ofs ty) m)
           | _ => stuck
           end
       | Some _ =>
@@ -769,20 +773,20 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       | Some(b, ofs, ty') =>
           check type_eq ty ty';
           do w',t,v <- do_deref_loc w ty m b ofs;
-          topred (Rred (Eval v ty) m t)
+          topred (Rred "red_rvalof" (Eval v ty) m t)
       | None =>
           incontext (fun x => Evalof x ty) (step_expr LV l m)
       end
   | RV, Eaddrof l ty =>
       match is_loc l with
-      | Some(b, ofs, ty') => topred (Rred (Eval (Vptr b ofs) ty) m E0)
+      | Some(b, ofs, ty') => topred (Rred "red_addrof" (Eval (Vptr b ofs) ty) m E0)
       | None => incontext (fun x => Eaddrof x ty) (step_expr LV l m)
       end
   | RV, Eunop op r1 ty =>
       match is_val r1 with
       | Some(v1, ty1) =>
           do v <- sem_unary_operation op v1 ty1;
-          topred (Rred (Eval v ty) m E0)
+          topred (Rred "red_unop" (Eval v ty) m E0)
       | None =>
           incontext (fun x => Eunop op x ty) (step_expr RV r1 m)
       end
@@ -790,7 +794,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1, is_val r2 with
       | Some(v1, ty1), Some(v2, ty2) =>
           do v <- sem_binary_operation ge op v1 ty1 v2 ty2 m;
-          topred (Rred (Eval v ty) m E0)
+          topred (Rred "red_binop" (Eval v ty) m E0)
       | _, _ =>
          incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m)
                     (fun x => Ebinop op r1 x ty) (step_expr RV r2 m)
@@ -799,7 +803,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some(v1, ty1) =>
           do v <- sem_cast v1 ty1 ty;
-          topred (Rred (Eval v ty) m E0)
+          topred (Rred "red_cast" (Eval v ty) m E0)
       | None =>
           incontext (fun x => Ecast x ty) (step_expr RV r1 m)
       end
@@ -807,8 +811,8 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some(v1, ty1) =>
           do b <- bool_val v1 ty1;
-          if b then topred (Rred (Eparen r2 type_bool ty) m E0)
-               else topred (Rred (Eval (Vint Int.zero) ty) m E0)
+          if b then topred (Rred "red_seqand_true" (Eparen r2 type_bool ty) m E0)
+               else topred (Rred "red_seqand_false" (Eval (Vint Int.zero) ty) m E0)
       | None =>
           incontext (fun x => Eseqand x r2 ty) (step_expr RV r1 m)
       end
@@ -816,8 +820,8 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some(v1, ty1) =>
           do b <- bool_val v1 ty1;
-          if b then topred (Rred (Eval (Vint Int.one) ty) m E0)
-               else topred (Rred (Eparen r2 type_bool ty) m E0)
+          if b then topred (Rred "red_seqor_true" (Eval (Vint Int.one) ty) m E0)
+               else topred (Rred "red_seqor_false" (Eparen r2 type_bool ty) m E0)
       | None =>
           incontext (fun x => Eseqor x r2 ty) (step_expr RV r1 m)
       end
@@ -825,21 +829,21 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some(v1, ty1) =>
           do b <- bool_val v1 ty1;
-          topred (Rred (Eparen (if b then r2 else r3) ty ty) m E0)
+          topred (Rred "red_condition" (Eparen (if b then r2 else r3) ty ty) m E0)
       | None =>
           incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m)
       end
   | RV, Esizeof ty' ty =>
-      topred (Rred (Eval (Vint (Int.repr (sizeof ge ty'))) ty) m E0)
+      topred (Rred "red_sizeof" (Eval (Vint (Int.repr (sizeof ge ty'))) ty) m E0)
   | RV, Ealignof ty' ty =>
-      topred (Rred (Eval (Vint (Int.repr (alignof ge ty'))) ty) m E0)
+      topred (Rred "red_alignof" (Eval (Vint (Int.repr (alignof ge ty'))) ty) m E0)
   | RV, Eassign l1 r2 ty =>
       match is_loc l1, is_val r2 with
       | Some(b, ofs, ty1), Some(v2, ty2) =>
           check type_eq ty1 ty;
           do v <- sem_cast v2 ty2 ty1;
           do w',t,m' <- do_assign_loc w ty1 m b ofs v;
-          topred (Rred (Eval v ty) m' t)
+          topred (Rred "red_assign" (Eval v ty) m' t)
       | _, _ =>
          incontext2 (fun x => Eassign x r2 ty) (step_expr LV l1 m)
                     (fun x => Eassign l1 x ty) (step_expr RV r2 m)
@@ -851,7 +855,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
           do w',t,v1 <- do_deref_loc w ty1 m b ofs;
           let r' := Eassign (Eloc b ofs ty1)
                            (Ebinop op (Eval v1 ty1) (Eval v2 ty2) tyres) ty1 in
-          topred (Rred r' m t)
+          topred (Rred "red_assignop" r' m t)
       | _, _ =>
          incontext2 (fun x => Eassignop op x r2 tyres ty) (step_expr LV l1 m)
                     (fun x => Eassignop op l1 x tyres ty) (step_expr RV r2 m)
@@ -867,7 +871,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
                            (Ebinop op (Eval v1 ty) (Eval (Vint Int.one) type_int32s) (incrdecr_type ty))
                            ty)
                    (Eval v1 ty) ty in
-          topred (Rred r' m t)
+          topred (Rred "red_postincr" r' m t)
       | None =>
           incontext (fun x => Epostincr id x ty) (step_expr LV l m)
       end
@@ -875,7 +879,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some _ =>
           check type_eq (typeof r2) ty;
-          topred (Rred r2 m E0)
+          topred (Rred "red_comma" r2 m E0)
       | None =>
           incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m)
       end
@@ -883,7 +887,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some (v1, ty1) =>
           do v <- sem_cast v1 ty1 tycast;
-          topred (Rred (Eval v ty) m E0)
+          topred (Rred "red_paren" (Eval v ty) m E0)
       | None =>
           incontext (fun x => Eparen x tycast ty) (step_expr RV r1 m)
       end
@@ -895,7 +899,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
               do fd <- Genv.find_funct ge vf;
               do vargs <- sem_cast_arguments vtl tyargs;
               check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv);
-              topred (Callred fd vargs ty m)
+              topred (Callred "red_call" fd vargs ty m)
           | _ => stuck
           end
       | _, _ =>
@@ -908,7 +912,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
           do vargs <- sem_cast_arguments vtl tyargs;
           match do_external ef w vargs m with
           | None => stuck
-          | Some(w',t,v,m') => topred (Rred (Eval v ty) m' t)
+          | Some(w',t,v,m') => topred (Rred "red_builtin" (Eval v ty) m' t)
           end
       | _ =>
           incontext (fun x => Ebuiltin ef tyargs x ty) (step_exprlist rargs m)
@@ -956,21 +960,6 @@ Proof.
   eapply imm_safe_callred; eauto.
 Qed.
 
-(*
-Definition not_stuck (a: expr) (m: mem) :=
-  forall a' k C, context k RV C -> a = C a' -> imm_safe_t k a' m.
-
-Lemma safe_expr_kind:
-  forall k C a m,
-  context k RV C ->
-  not_stuck (C a) m ->
-  k = Cstrategy.expr_kind a.
-Proof.
-  intros.
-  symmetry. eapply Cstrategy.imm_safe_kind. eapply imm_safe_t_imm_safe. eauto.
-Qed.
-*)
-
 Fixpoint exprlist_all_values (rl: exprlist) : Prop :=
   match rl with
   | Enil => True
@@ -1163,9 +1152,9 @@ Hint Resolve context_compose contextlist_compose.
 
 Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop :=
   match k, rd with
-  | LV, Lred l' m' => lred ge e a m l' m'
-  | RV, Rred r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w'
-  | RV, Callred fd args tyres m' => callred ge a fd args tyres /\ m' = m
+  | LV, Lred _ l' m' => lred ge e a m l' m'
+  | RV, Rred _ r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w'
+  | RV, Callred _ fd args tyres m' => callred ge a fd args tyres /\ m' = m
   | LV, Stuckred => ~imm_safe_t k a m
   | RV, Stuckred => ~imm_safe_t k a m
   | _, _ => False
@@ -1521,7 +1510,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   destruct (Genv.find_funct ge vf) as [fd|] eqn:?...
   destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... 
   destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))...
-  apply topred_ok; auto. red. split; auto. eapply red_Ecall; eauto. 
+  apply topred_ok; auto. red. split; auto. eapply red_call; eauto. 
   eapply sem_cast_arguments_sound; eauto.
   apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence.
   apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv.
@@ -1583,73 +1572,77 @@ Qed.
 Lemma lred_topred:
   forall l1 m1 l2 m2,
   lred ge e l1 m1 l2 m2 ->
-  step_expr LV l1 m1 = topred (Lred l2 m2).
+  exists rule, step_expr LV l1 m1 = topred (Lred rule l2 m2).
 Proof.
   induction 1; simpl.
 (* var local *)
-  rewrite H. rewrite dec_eq_true; auto.
+  rewrite H. rewrite dec_eq_true. econstructor; eauto.
 (* var global *)
-  rewrite H; rewrite H0. auto.
+  rewrite H; rewrite H0. econstructor; eauto.
 (* deref *) 
-  auto.
+  econstructor; eauto.
 (* field struct *)
-  rewrite H, H0; auto.
+  rewrite H, H0; econstructor; eauto.
 (* field union *)
-  rewrite H; auto.
+  rewrite H; econstructor; eauto.
 Qed.
 
 Lemma rred_topred:
   forall w' r1 m1 t r2 m2,
   rred ge r1 m1 t r2 m2 -> possible_trace w t w' ->
-  step_expr RV r1 m1 = topred (Rred r2 m2 t).
+  exists rule, step_expr RV r1 m1 = topred (Rred rule r2 m2 t).
 Proof.
   induction 1; simpl; intros.
 (* valof *)
-  rewrite dec_eq_true; auto. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). auto. 
+  rewrite dec_eq_true. 
+  rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). econstructor; eauto.
 (* addrof *)
-  inv H. auto.
+  inv H. econstructor; eauto.
 (* unop *)
-  inv H0. rewrite H; auto.
+  inv H0. rewrite H; econstructor; eauto.
 (* binop *)
-  inv H0. rewrite H; auto.
+  inv H0. rewrite H; econstructor; eauto.
 (* cast *)
-  inv H0. rewrite H; auto.
+  inv H0. rewrite H; econstructor; eauto.
 (* seqand *)
-  inv H0. rewrite H; auto.
-  inv H0. rewrite H; auto.
+  inv H0. rewrite H; econstructor; eauto.
+  inv H0. rewrite H; econstructor; eauto.
 (* seqor *)
-  inv H0. rewrite H; auto.
-  inv H0. rewrite H; auto.
+  inv H0. rewrite H; econstructor; eauto.
+  inv H0. rewrite H; econstructor; eauto.
 (* condition *)
-  inv H0. rewrite H; auto.
+  inv H0. rewrite H; econstructor; eauto.
 (* sizeof *)
-  inv H. auto.
+  inv H. econstructor; eauto.
 (* alignof *)
-  inv H. auto.
+  inv H. econstructor; eauto.
 (* assign *)
-  rewrite dec_eq_true; auto. rewrite H. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H1). auto.
+  rewrite dec_eq_true. rewrite H. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H1).
+  econstructor; eauto.
 (* assignop *)
-  rewrite dec_eq_true; auto. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). auto. 
+  rewrite dec_eq_true. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0).
+  econstructor; eauto. 
 (* postincr *)
-  rewrite dec_eq_true; auto. subst. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H1). auto.
+  rewrite dec_eq_true. subst. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H1).
+  econstructor; eauto.
 (* comma *)
-  inv H0. rewrite dec_eq_true; auto.
+  inv H0. rewrite dec_eq_true. econstructor; eauto.
 (* paren *)
-  inv H0. rewrite H; auto.
+  inv H0. rewrite H; econstructor; eauto.
 (* builtin *)
   exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]].
   exploit do_ef_external_complete; eauto. intros C. 
-  rewrite A. rewrite B. rewrite C. auto.
+  rewrite A. rewrite B. rewrite C. econstructor; eauto.
 Qed.
 
 Lemma callred_topred:
   forall a fd args ty m,
   callred ge a fd args ty ->
-  step_expr RV a m = topred (Callred fd args ty m).
+  exists rule, step_expr RV a m = topred (Callred rule fd args ty m).
 Proof.
   induction 1; simpl.
   rewrite H2. exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]].
-  rewrite A; rewrite H; rewrite B; rewrite H1; rewrite dec_eq_true. auto.
+  rewrite A; rewrite H; rewrite B; rewrite H1; rewrite dec_eq_true. econstructor; eauto.
 Qed.
 
 Definition reducts_incl {A B: Type} (C: A -> B) (res1: reducts A) (res2: reducts B) : Prop :=
@@ -1956,44 +1949,54 @@ Proof.
    simpl. auto. 
 Qed.
 
+Inductive transition : Type := TR (rule: string) (t: trace) (S': state).
+
 Definition expr_final_state (f: function) (k: cont) (e: env) (C_rd: (expr -> expr) * reduction) :=
   match snd C_rd with
-  | Lred a m => (E0, ExprState f (fst C_rd a) k e m)
-  | Rred a m t => (t, ExprState f (fst C_rd a) k e m)
-  | Callred fd vargs ty m => (E0, Callstate fd vargs (Kcall f e (fst C_rd) ty k) m)
-  | Stuck => (E0, Stuckstate)
+  | Lred rule a m => TR rule E0 (ExprState f (fst C_rd a) k e m)
+  | Rred rule a m t => TR rule t (ExprState f (fst C_rd a) k e m)
+  | Callred rule fd vargs ty m => TR rule E0 (Callstate fd vargs (Kcall f e (fst C_rd) ty k) m)
+  | Stuckred => TR "step_stuck" E0 Stuckstate
   end.
 
 Local Open Scope list_monad_scope.
 
-Definition ret (S: state) : list (trace * state) := (E0, S) :: nil.
+Definition ret (rule: string) (S: state) : list transition :=
+  TR rule E0 S :: nil.
 
-Definition do_step (w: world) (s: state) : list (trace * state) :=
+Definition do_step (w: world) (s: state) : list transition :=
   match s with
 
   | ExprState f a k e m =>
       match is_val a with
       | Some(v, ty) =>
         match k with
-        | Kdo k => ret (State f Sskip k e m )
+        | Kdo k => ret "step_do_2" (State f Sskip k e m )
         | Kifthenelse s1 s2 k =>
-            do b <- bool_val v ty; ret (State f (if b then s1 else s2) k e m)
+            do b <- bool_val v ty;
+            ret "step_ifthenelse_2" (State f (if b then s1 else s2) k e m)
         | Kwhile1 x s k =>
             do b <- bool_val v ty; 
-            if b then ret (State f s (Kwhile2 x s k) e m) else ret (State f Sskip k e m)
+            if b
+            then ret "step_while_true" (State f s (Kwhile2 x s k) e m)
+            else ret "step_while_false" (State f Sskip k e m)
         | Kdowhile2 x s k =>
             do b <- bool_val v ty;
-            if b then ret (State f (Sdowhile x s) k e m) else ret (State f Sskip k e m)
+            if b
+            then ret "step_dowhile_true" (State f (Sdowhile x s) k e m)
+            else ret "step_dowhile_false" (State f Sskip k e m)
         | Kfor2 a2 a3 s k =>
             do b <- bool_val v ty;
-            if b then ret (State f s (Kfor3 a2 a3 s k) e m) else ret (State f Sskip k e m)
+            if b
+            then ret "step_for_true" (State f s (Kfor3 a2 a3 s k) e m)
+            else ret "step_for_false" (State f Sskip k e m)
         | Kreturn k =>
             do v' <- sem_cast v ty f.(fn_return);
             do m' <- Mem.free_list m (blocks_of_env ge e);
-            ret (Returnstate v' (call_cont k) m')
+            ret "step_return_2" (Returnstate v' (call_cont k) m')
         | Kswitch1 sl k =>
             do n <- sem_switch_arg v ty;
-            ret (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m)
+            ret "step_expr_switch" (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m)
         | _ => nil
         end
 
@@ -2001,48 +2004,66 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
           map (expr_final_state f k e) (step_expr e w RV a m)
       end
 
-  | State f (Sdo x) k e m => ret(ExprState f x (Kdo k) e m)
-
-  | State f (Ssequence s1 s2) k e m => ret(State f s1 (Kseq s2 k) e m)
-  | State f Sskip (Kseq s k) e m => ret (State f s k e m)
-  | State f Scontinue (Kseq s k) e m => ret (State f Scontinue k e m)
-  | State f Sbreak (Kseq s k) e m => ret (State f Sbreak k e m)
-
-  | State f (Sifthenelse a s1 s2) k e m => ret (ExprState f a (Kifthenelse s1 s2 k) e m)
-
-  | State f (Swhile x s) k e m => ret (ExprState f x (Kwhile1 x s k) e m)
-  | State f (Sskip|Scontinue) (Kwhile2 x s k) e m => ret (State f (Swhile x s) k e m)
-  | State f Sbreak (Kwhile2 x s k) e m => ret (State f Sskip k e m)
-
-  | State f (Sdowhile a s) k e m => ret (State f s (Kdowhile1 a s k) e m)
-  | State f (Sskip|Scontinue) (Kdowhile1 x s k) e m => ret (ExprState f x (Kdowhile2 x s k) e m)
-  | State f Sbreak (Kdowhile1 x s k) e m => ret (State f Sskip k e m)
+  | State f (Sdo x) k e m =>
+      ret "step_do_1" (ExprState f x (Kdo k) e m)
+  | State f (Ssequence s1 s2) k e m =>
+      ret "step_seq" (State f s1 (Kseq s2 k) e m)
+  | State f Sskip (Kseq s k) e m =>
+      ret "step_skip_seq" (State f s k e m)
+  | State f Scontinue (Kseq s k) e m =>
+      ret "step_continue_seq" (State f Scontinue k e m)
+  | State f Sbreak (Kseq s k) e m =>
+      ret "step_break_seq" (State f Sbreak k e m)
+
+  | State f (Sifthenelse a s1 s2) k e m =>
+      ret "step_ifthenelse_1" (ExprState f a (Kifthenelse s1 s2 k) e m)
+
+  | State f (Swhile x s) k e m =>
+      ret "step_while" (ExprState f x (Kwhile1 x s k) e m)
+  | State f (Sskip|Scontinue) (Kwhile2 x s k) e m =>
+      ret "step_skip_or_continue_while" (State f (Swhile x s) k e m)
+  | State f Sbreak (Kwhile2 x s k) e m =>
+      ret "step_break_while" (State f Sskip k e m)
+
+  | State f (Sdowhile a s) k e m =>
+      ret "step_dowhile" (State f s (Kdowhile1 a s k) e m)
+  | State f (Sskip|Scontinue) (Kdowhile1 x s k) e m =>
+      ret "step_skip_or_continue_dowhile" (ExprState f x (Kdowhile2 x s k) e m)
+  | State f Sbreak (Kdowhile1 x s k) e m =>
+      ret "step_break_dowhile" (State f Sskip k e m)
 
   | State f (Sfor a1 a2 a3 s) k e m =>
       if is_skip a1
-      then ret (ExprState f a2 (Kfor2 a2 a3 s k) e m)
-      else ret (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
-  | State f Sskip (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m)
-  | State f Scontinue (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m)
-  | State f Sbreak (Kfor3 a2 a3 s k) e m => ret (State f Sskip k e m)
-  | State f Sskip (Kfor4 a2 a3 s k) e m => ret (State f (Sfor Sskip a2 a3 s) k e m)
+      then ret "step_for" (ExprState f a2 (Kfor2 a2 a3 s k) e m)
+      else ret "step_for_start" (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
+  | State f (Sskip|Scontinue) (Kfor3 a2 a3 s k) e m =>
+      ret "step_skip_or_continue_for3" (State f a3 (Kfor4 a2 a3 s k) e m)
+  | State f Sbreak (Kfor3 a2 a3 s k) e m =>
+      ret "step_break_for3" (State f Sskip k e m)
+  | State f Sskip (Kfor4 a2 a3 s k) e m =>
+      ret "step_skip_for4" (State f (Sfor Sskip a2 a3 s) k e m)
 
   | State f (Sreturn None) k e m =>
       do m' <- Mem.free_list m (blocks_of_env ge e);
-      ret (Returnstate Vundef (call_cont k) m')
-  | State f (Sreturn (Some x)) k e m => ret (ExprState f x (Kreturn k) e m)
+      ret "step_return_0" (Returnstate Vundef (call_cont k) m')
+  | State f (Sreturn (Some x)) k e m =>
+      ret "step_return_1" (ExprState f x (Kreturn k) e m)
   | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => 
       do m' <- Mem.free_list m (blocks_of_env ge e);
-      ret (Returnstate Vundef k m')
+      ret "step_skip_call" (Returnstate Vundef k m')
 
-  | State f (Sswitch x sl) k e m => ret (ExprState f x (Kswitch1 sl k) e m)
-  | State f (Sskip|Sbreak) (Kswitch2 k) e m => ret (State f Sskip k e m)
-  | State f Scontinue (Kswitch2 k) e m => ret (State f Scontinue k e m)
+  | State f (Sswitch x sl) k e m =>
+      ret "step_switch" (ExprState f x (Kswitch1 sl k) e m)
+  | State f (Sskip|Sbreak) (Kswitch2 k) e m =>
+      ret "step_skip_break_switch" (State f Sskip k e m)
+  | State f Scontinue (Kswitch2 k) e m =>
+      ret "step_continue_switch" (State f Scontinue k e m)
 
-  | State f (Slabel lbl s) k e m => ret (State f s k e m)
+  | State f (Slabel lbl s) k e m =>
+      ret "step_label" (State f s k e m)
   | State f (Sgoto lbl) k e m =>
       match find_label lbl f.(fn_body) (call_cont k) with
-      | Some(s', k') => ret (State f s' k' e m)
+      | Some(s', k') => ret "step_goto" (State f s' k' e m)
       | None => nil
       end
 
@@ -2050,14 +2071,15 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
       check (list_norepet_dec ident_eq (var_names (fn_params f) ++ var_names (fn_vars f)));
       let (e,m1) := do_alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) in
       do m2 <- sem_bind_parameters w e m1 f.(fn_params) vargs;
-      ret (State f f.(fn_body) k e m2)
+      ret "step_internal_function" (State f f.(fn_body) k e m2)
   | Callstate (External ef _ _ _) vargs k m =>
       match do_external ef w vargs m with
       | None => nil
-      | Some(w',t,v,m') => (t, Returnstate v k m') :: nil
+      | Some(w',t,v,m') => TR "step_external_function" t (Returnstate v k m') :: nil
       end
 
-  | Returnstate v (Kcall f e C ty k) m => ret (ExprState f (C (Eval v ty)) k e m)
+  | Returnstate v (Kcall f e C ty k) m =>
+      ret "step_returnstate" (ExprState f (C (Eval v ty)) k e m)
 
   | _ => nil
   end.
@@ -2065,7 +2087,7 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
 Ltac myinv :=
   match goal with
   | [ |- In _ nil -> _ ] => intro X; elim X
-  | [ |- In _ (ret _) -> _ ] => 
+  | [ |- In _ (ret _ _) -> _ ] => 
         intro X; elim X; clear X;
         [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
   | [ |- In _ (_ :: nil) -> _ ] => 
@@ -2079,8 +2101,8 @@ Ltac myinv :=
 Hint Extern 3 => exact I.
 
 Theorem do_step_sound:
-  forall w S t S',
-  In (t, S') (do_step w S) ->
+  forall w S rule t S',
+  In (TR rule t S') (do_step w S) ->
   Csem.step ge S t S' \/ (t = E0 /\ S' = Stuckstate /\ can_crash_world w S).
 Proof with try (left; right; econstructor; eauto; fail).
   intros until S'. destruct S; simpl.
@@ -2145,45 +2167,52 @@ Proof.
 Qed.
 
 Theorem do_step_complete:
-  forall w S t S' w', possible_trace w t w' -> Csem.step ge S t S' -> In (t, S') (do_step w S).
-Proof with (unfold ret; auto with coqlib).
+  forall w S t S' w',
+  possible_trace w t w' -> Csem.step ge S t S' -> exists rule, In (TR rule t S') (do_step w S).
+Proof with (unfold ret; eauto with coqlib).
   intros until w'; intros PT H.
   destruct H. 
   (* Expression step *)
   inversion H; subst; exploit estep_not_val; eauto; intro NOTVAL.
 (* lred *)
   unfold do_step; rewrite NOTVAL.
-  change (E0, ExprState f (C a') k e m') with (expr_final_state f k e (C, Lred a' m')).
+  exploit lred_topred; eauto. instantiate (1 := w). intros (rule & STEP).
+  exists rule. change (TR rule E0 (ExprState f (C a') k e m')) with (expr_final_state f k e (C, Lred rule a' m')).
   apply in_map.
   generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl.
-  intro. replace C with (fun x => C x). apply H2. 
-  rewrite (lred_topred _ _ _ _ _ _ H0). unfold topred; auto with coqlib.
+  intro. replace C with (fun x => C x). apply H2.
+  rewrite STEP. unfold topred; auto with coqlib.
   apply extensionality; auto.
 (* rred *)
   unfold do_step; rewrite NOTVAL.
-  change (t, ExprState f (C a') k e m') with (expr_final_state f k e (C, Rred a' m' t)).
+  exploit rred_topred; eauto. instantiate (1 := e). intros (rule & STEP).
+  exists rule.
+  change (TR rule t (ExprState f (C a') k e m')) with (expr_final_state f k e (C, Rred rule a' m' t)).
   apply in_map.
   generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl.
-  intro. replace C with (fun x => C x). apply H2. 
-  rewrite (rred_topred _ _ _ _ _ _ _ _ H0 PT). unfold topred; auto with coqlib.
+  intro. replace C with (fun x => C x). apply H2.
+  rewrite STEP; unfold topred; auto with coqlib.
   apply extensionality; auto.
 (* callred *)
   unfold do_step; rewrite NOTVAL.
-  change (E0, Callstate fd vargs (Kcall f e C ty k) m) with (expr_final_state f k e (C, Callred fd vargs ty m)).
+  exploit callred_topred; eauto. instantiate (1 := m). instantiate (1 := w). instantiate (1 := e).
+  intros (rule & STEP). exists rule.
+  change (TR rule E0 (Callstate fd vargs (Kcall f e C ty k) m)) with (expr_final_state f k e (C, Callred rule fd vargs ty m)).
   apply in_map.
   generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl.
   intro. replace C with (fun x => C x). apply H2. 
-  rewrite (callred_topred _ _ _ _ _ _ _ H0). unfold topred; auto with coqlib.
+  rewrite STEP; unfold topred; auto with coqlib.
   apply extensionality; auto.
 (* stuck *)
   exploit not_imm_safe_stuck_red. eauto. red; intros; elim H1. eapply imm_safe_t_imm_safe. eauto.
   instantiate (1 := w). intros [C' IN].
-  simpl do_step. rewrite NOTVAL. 
-  change (E0, Stuckstate) with (expr_final_state f k e (C', Stuckred)).
+  simpl do_step. rewrite NOTVAL.
+  exists "step_stuck".
+  change (TR "step_stuck" E0 Stuckstate) with (expr_final_state f k e (C', Stuckred)).
   apply in_map. auto. 
 
   (* Statement step *)
-  inv H; simpl...
+  inv H; simpl; econstructor...
   rewrite H0...
   rewrite H0...
   rewrite H0...
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index e6e3a321..fafbf29f 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -317,7 +317,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop :=
     (More exactly, identification of function calls that can reduce.) *)
 
 Inductive callred: expr -> fundef -> list val -> type -> Prop :=
-  | red_Ecall: forall vf tyf tyargs tyres cconv el ty fd vargs,
+  | red_call: forall vf tyf tyargs tyres cconv el ty fd vargs,
       Genv.find_funct ge vf = Some fd ->
       cast_arguments el tyargs vargs ->
       type_of_fundef fd = Tfunction tyargs tyres cconv ->
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index bad92cf6..612103a6 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -224,16 +224,21 @@ let elab_char_constant loc wide chars =
   let v =
     List.fold_left 
       (fun acc d ->
-        if acc >= max_val then
+        if acc < 0L || acc >= max_val then
           error loc "character constant overflows";
-        if d >= max_digit then
-          warning loc "escape sequence is out of range (code 0x%LX)" d;
+        if d < 0L || d >= max_digit then
+          error loc "escape sequence is out of range (code 0x%LX)" d;
         Int64.add (Int64.shift_left acc nbits) d)
       0L chars in
   if not (integer_representable v IInt) then
     warning loc "character constant cannot be represented at type 'int'";
-  (* C99 6.4.4.4 item 10: single character -> represent at type char *)
-  Ceval.normalize_int v (if List.length chars = 1 then IChar else IInt)
+  (* C99 6.4.4.4 item 10: single character -> represent at type char
+     or wchar_t *)
+  Ceval.normalize_int v
+    (if List.length chars = 1 then
+       if wide then wchar_ikind() else IChar
+     else
+       IInt)
 
 let elab_string_literal loc wide chars =
   let nbits = if wide then 8 * !config.sizeof_wchar else 8 in 
@@ -241,14 +246,14 @@ let elab_string_literal loc wide chars =
   List.iter
     (fun c ->
       if c < 0L || c >= char_max
-      then warning loc "escape sequence is out of range (code 0x%LX)" c)
+      then error loc "escape sequence is out of range (code 0x%LX)" c)
     chars;
   if wide then
     CWStr chars
   else begin
     let res = String.create (List.length chars) in
     List.iteri
-      (fun i c -> res.[i] <- Char.chr (Int64.to_int c))
+      (fun i c -> res.[i] <- Char.unsafe_chr (Int64.to_int c))
       chars;
     CStr res
   end
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index e73125f7..0012dc0c 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -10,86 +10,87 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+open Printf
 
-let config_vars: (string, string) Hashtbl.t = Hashtbl.create 10
+(* Locate the .ini file, which is either in the same directory as
+  the executable or in the directory ../share *)
 
+let ini_file_name =
+  try
+    Sys.getenv "COMPCERT_CONFIG"
+  with Not_found ->
+    let exe_dir = Filename.dirname Sys.executable_name in
+    let exe_ini = Filename.concat exe_dir "compcert.ini" in
+    let share_dir =
+      Filename.concat (Filename.concat exe_dir Filename.parent_dir_name)
+                      "share" in
+    let share_ini = Filename.concat share_dir "compcert.ini" in
+    if Sys.file_exists exe_ini then exe_ini
+    else if Sys.file_exists share_ini then share_ini
+    else begin 
+      eprintf "Cannot find compcert.ini configuration file.\n";
+      exit 2
+    end
+
+(* Read in the .ini file *)
 
-(* Read in the .ini file, which is either in the same directory or in the directory ../share *)
 let _ =
   try
-    let file = 
-      try
-        let env_file = Sys.getenv "COMPCERT_CONFIG" in
-        open_in env_file
-      with Not_found ->
-        let dir = Sys.getcwd () 
-        and name = Sys.executable_name in
-        let dirname = if Filename.is_relative name then
-          Filename.dirname (Filename.concat dir name)
-        else 
-          Filename.dirname name
-        in
-        let share_dir = Filename.concat (Filename.concat dirname Filename.parent_dir_name) "share" in
-        try
-          open_in (Filename.concat dirname "compcert.ini")
-        with Sys_error _ ->
-          open_in (Filename.concat share_dir "compcert.ini")
-    in
-    (try
-      let ini_line = Str.regexp "\\([^=]+\\)=\\(.+\\)" in
-      while true do
-        let line = input_line file in
-        if Str.string_match ini_line line 0 then
-          let key = Str.matched_group 1 line
-          and value = Str.matched_group 2 line in
-          Hashtbl.add config_vars key value
-        else
-          Printf.eprintf "Wrong value %s in .ini file.\n" line
-      done
-    with End_of_file -> close_in file)
-  with Sys_error msg -> Printf.eprintf "Unable to open .ini file\n"
+    Readconfig.read_config_file ini_file_name
+  with
+  | Readconfig.Error(file, lineno, msg) ->
+      eprintf "Error reading configuration file %s.\n" ini_file_name;
+      eprintf "%s:%d:%s\n" file lineno msg;
+      exit 2
+  | Sys_error msg ->
+      eprintf "Error reading configuration file %s.\n" ini_file_name;
+      eprintf "%s\n" msg;
+      exit 2
 
 let get_config key =
-  try
-    Hashtbl.find config_vars key
-  with Not_found ->
-    Printf.eprintf "Configuration option `%s' is not set\n" key; exit 2
+  match Readconfig.key_val key with
+  | Some v -> v
+  | None -> eprintf "Configuration option `%s' is not set\n" key; exit 2
 
-let bad_config key v =
-  Printf.eprintf "Invalid value `%s' for configuation option `%s'\n" v key; exit 2
+let bad_config key vl =
+  eprintf "Invalid value `%s' for configuration option `%s'\n"
+          (String.concat " " vl) key;
+  exit 2
 
-let prepro = get_config "prepro"
-let asm = get_config "asm"
-let linker = get_config "linker"
-let arch = 
-  let v = get_config "arch" in
-  (match v with
-  | "powerpc"
-  | "arm"
-  | "ia32" -> ()
-  | _ -> bad_config "arch" v);
-  v
+let get_config_string key =
+  match get_config key with
+  | [v] -> v
+  | vl -> bad_config key vl
 
-let model = get_config "model"
-let abi = get_config "abi"
-let system = get_config "system"
+let get_config_list key =
+  match get_config key with
+  | [] -> bad_config key []
+  | vl -> vl
+
+let prepro = get_config_list "prepro"
+let asm = get_config_list "asm"
+let linker = get_config_list "linker"
+let arch = 
+  match get_config_string "arch" with
+  | "powerpc"|"arm"|"ia32" as a -> a
+  | v -> bad_config "arch" [v]
+let model = get_config_string "model"
+let abi = get_config_string "abi"
+let system = get_config_string "system"
 let has_runtime_lib = 
-  match get_config "has_runtime_lib" with
+  match get_config_string "has_runtime_lib" with
   | "true" -> true
   | "false" -> false
-  | v -> bad_config "has_runtime_lib" v
-
-
+  | v -> bad_config "has_runtime_lib" [v]
 let stdlib_path =
   if has_runtime_lib then
-    get_config "stdlib_path"
+    get_config_string "stdlib_path"
   else
     ""
-
 let asm_supports_cfi = 
-  match get_config "asm_supports_cfi" with
+  match get_config_string "asm_supports_cfi" with
   | "true" -> true
   | "false" -> false
-  | v -> bad_config "asm_supports_cfi" v
+  | v -> bad_config "asm_supports_cfi" [v]
 
-let version = get_config "version"
+let version = get_config_string "version"
diff --git a/driver/Driver.ml b/driver/Driver.ml
index e943e6c9..d8b28285 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -20,17 +20,38 @@ open Timing
 
 let stdlib_path = ref Configuration.stdlib_path
 
-let command cmd =
+(* Invocation of external tools *)
+
+let command ?stdout args =
   if !option_v then begin
-    prerr_string "+ "; prerr_string cmd; prerr_endline ""
+    eprintf "+ %s" (String.concat " " args);
+    begin match stdout with
+    | None -> ()
+    | Some f -> eprintf " > %s" f
+    end;
+    prerr_endline ""
   end;
-  Sys.command cmd
-
-let quote_options opts =
-  String.concat " " (List.rev_map Filename.quote opts)
-
-let quote_arguments args =
-  String.concat " " (List.map Filename.quote args)
+  let argv = Array.of_list args in
+  assert (Array.length argv > 0);
+  try
+    let fd_out =
+      match stdout with
+      | None -> Unix.stdout
+      | Some f ->
+          Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in
+    let pid =
+      Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in
+    let (_, status) =
+      Unix.waitpid [] pid in
+    if stdout <> None then Unix.close fd_out;
+    match status with
+    | Unix.WEXITED rc -> rc
+    | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+        eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
+  with Unix.Unix_error(err, fn, param) ->
+    eprintf "Error executing '%s': %s: %s %s\n"
+            argv.(0) fn (Unix.error_message err) param;
+    -1
 
 let safe_remove file =
   try Sys.remove file with Sys_error _ -> ()
@@ -68,16 +89,17 @@ let output_filename_default default_file =
 
 let preprocess ifile ofile =
   let output =
-    if ofile = "-" then "" else sprintf "> %s" ofile in
-  let cmd =
-    sprintf "%s -D__COMPCERT__ %s %s %s %s"
-      Configuration.prepro
-      (if Configuration.has_runtime_lib
-       then sprintf "-I%s" !stdlib_path
-       else "")
-      (quote_options !prepro_options)
-      ifile output in
-  if command cmd <> 0 then begin
+    if ofile = "-" then None else Some ofile in
+  let cmd = List.concat [
+    Configuration.prepro;
+    ["-D__COMPCERT__"];
+    (if Configuration.has_runtime_lib
+     then ["-I" ^ !stdlib_path]
+     else []);
+    List.rev !prepro_options;
+    [ifile]
+  ] in
+  if command ?stdout:output cmd <> 0 then begin
     if ofile <> "-" then safe_remove ofile;
     eprintf "Error during preprocessing.\n";
     exit 2
@@ -208,11 +230,13 @@ let compile_cminor_file ifile ofile =
 (* From asm to object file *)
 
 let assemble ifile ofile =
-  let cmd =
-    sprintf "%s -o %s %s %s"
-      Configuration.asm ofile (quote_options !assembler_options) ifile in
-  let retcode = command cmd in
-  if retcode <> 0 then begin
+  let cmd = List.concat [
+    Configuration.asm;
+    ["-o"; ofile];
+    List.rev !assembler_options;
+    [ifile]
+  ] in
+  if command cmd <> 0 then begin
     safe_remove ofile;
     eprintf "Error during assembling.\n";
     exit 2
@@ -221,14 +245,14 @@ let assemble ifile ofile =
 (* Linking *)
 
 let linker exe_name files =
-  let cmd =
-    sprintf "%s -o %s %s %s"
-      Configuration.linker
-      (Filename.quote exe_name)
-      (quote_arguments files)
-      (if Configuration.has_runtime_lib
-       then sprintf "-L%s -lcompcert" !stdlib_path
-       else "") in
+  let cmd = List.concat [
+    Configuration.linker;
+    ["-o"; exe_name];
+    files;
+    (if Configuration.has_runtime_lib
+     then ["-L" ^ !stdlib_path; "-lcompcert"]
+     else [])
+  ] in
   if command cmd <> 0 then exit 2
 
 (* Processing of a .c file *)
diff --git a/driver/Interp.ml b/driver/Interp.ml
index ab22cebb..2725dbfe 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -254,28 +254,14 @@ let compare_state s1 s2 =
       compare (rank_state s1) (rank_state s2)
   end
 
-(* Sets of states already explored *)
+(* Maps of states already explored. *)
 
-module StateSet =
-  Set.Make(struct
-             type t = state * Determinism.world
-             let compare (s1,w1) (s2,w2) = compare_state s1 s2
+module StateMap =
+  Map.Make(struct
+             type t = state
+             let compare = compare_state
            end)
 
-(* Purging states that will never be reached again based on their memory
-   next block.  All states with nextblock <= the given nextblock are
-   removed.  We take advantage of the fact that StateSets are sorted
-   by increasing nextblock, cf. the definition of compare_state above. *)
-
-let rec purge_seen nextblock seen =
-  let min = try Some(StateSet.min_elt seen) with Not_found -> None in
-  match min with
-  | None -> seen
-  | Some((s, w) as sw) ->
-      if P.le (mem_state s).Mem.nextblock nextblock
-      then purge_seen nextblock (StateSet.remove sw seen)
-      else seen
-
 (* Extract a string from a global pointer *)
 
 let extract_string m blk ofs =
@@ -435,7 +421,7 @@ and world_vstore ge m chunk id ofs ev =
 
 let do_event p ge time w ev =
   if !trace >= 1 then
-    fprintf p "@[<hov 2>Time %d: observable event:@ @[<hov 2>%a@]@]@."
+    fprintf p "@[<hov 2>Time %d: observable event:@ %a@]@."
               time print_event ev;
   (* Return new world after external action *)
   match ev with
@@ -497,11 +483,10 @@ let diagnose_stuck_state p ge w = function
   | ExprState(f,a,k,e,m) -> ignore(diagnose_stuck_expr p ge w f a k e m)
   | _ -> ()
 
-(* Exploration *)
+(* Execution of a single step.  Return list of triples
+   (reduction rule, next state, next world). *)
 
-let do_step p prog ge time (s, w) =
-  if !trace >= 2 then
-    fprintf p "@[<hov 2>Time %d: %a@]@." time print_state (prog, ge, s);
+let do_step p prog ge time s w =
   match Cexec.at_final_state s with
   | Some r ->
       if !trace >= 1 then
@@ -513,89 +498,71 @@ let do_step p prog ge time (s, w) =
       end
   | None ->
       let l = Cexec.do_step ge do_external_function do_inline_assembly w s in
-      if l = [] || List.exists (fun (t,s) -> s = Stuckstate) l then begin
+      if l = []
+      || List.exists (fun (Cexec.TR(r,t,s)) -> s = Stuckstate) l
+      then begin
         pp_set_max_boxes p 1000;
         fprintf p "@[<hov 2>Stuck state: %a@]@." print_state (prog, ge, s);
         diagnose_stuck_state p ge w s;
         fprintf p "ERROR: Undefined behavior@.";
         exit 126
       end else begin
-        List.map (fun (t, s') -> (s', do_events p ge time w t)) l
+        List.map (fun (Cexec.TR(r, t, s')) -> (r, s', do_events p ge time w t)) l
       end
 
-let rec explore_one p prog ge time sw =
-  let succs = do_step p prog ge time sw in
+(* Exploration of a single execution. *)
+
+let rec explore_one p prog ge time s w =
+  if !trace >= 2 then
+    fprintf p "@[<hov 2>Time %d:@ %a@]@." time print_state (prog, ge, s);
+  let succs = do_step p prog ge time s w in
   if succs <> [] then begin
-    let sw' =
+    let (r, s', w') =
       match !mode with
       | First -> List.hd succs
       | Random -> List.nth succs (Random.int (List.length succs))
       | All -> assert false in
-    explore_one p prog ge (time + 1) sw'
+    if !trace >= 2 then
+      fprintf p "--[%s]-->@." (camlstring_of_coqstring r);
+    explore_one p prog ge (time + 1) s' w'
   end
 
-(* A priority queue structure where the priority is inversely proportional
-   to the memory nextblock. *)
-
-module PrioQueue = struct
-
-  type elt = int * StateSet.elt
-
-  type queue = Empty | Node of elt * queue * queue
-
-  let empty = Empty
-
-  let singleton elt = Node(elt, Empty, Empty)
-
-  let higher_prio (time1, (s1, w1)) (time2, (s2, w2)) =
-    P.lt (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock
-
-  let rec insert queue elt =
-    match queue with
-    | Empty -> Node(elt, Empty, Empty)
-    | Node(e, left, right) ->
-        if higher_prio elt e
-        then Node(elt, insert right e, left)
-        else Node(e, insert right elt, left)
-
-  let rec remove_top = function
-  | Empty -> assert false
-  | Node(elt, left, Empty) -> left
-  | Node(elt, Empty, right) -> right
-  | Node(elt, (Node(lelt, _, _) as left),
-              (Node(relt, _, _) as right)) ->
-      if higher_prio lelt relt
-      then Node(lelt, remove_top left, right)
-      else Node(relt, left, remove_top right)
-
-  let extract = function
-  | Empty -> None
-  | Node(elt, _, _) as queue -> Some(elt, remove_top queue)
-
-  (* Return true if all elements of queue have strictly lower priority
-     than elt. *)
-  let dominate elt queue =
-    match queue with
-    | Empty -> true
-    | Node(e, _, _) -> higher_prio elt e
-end
-
-let rec explore_all p prog ge seen queue =
-  match PrioQueue.extract queue with
-  | None -> ()
-  | Some((time, sw) as tsw, queue') ->
-      if StateSet.mem sw seen then
-        explore_all p prog ge seen queue'
-      else
-        let succs = 
-          List.rev_map (fun sw -> (time + 1, sw)) (do_step p prog ge time sw) in
-        let queue'' = List.fold_left PrioQueue.insert queue' succs in
-        let seen' = StateSet.add sw seen in
-        let seen'' = 
-          if PrioQueue.dominate tsw queue''
-          then purge_seen (mem_state (fst sw)).Mem.nextblock seen'
-          else seen' in
-        explore_all p prog ge seen'' queue''
+(* Exploration of all possible executions. *)
+
+let rec explore_all p prog ge time states =
+  if !trace >= 2 then begin
+    List.iter
+      (fun (n, s, w) ->
+         fprintf p "@[<hov 2>State %d.%d: @ %a@]@."
+                   time n print_state (prog, ge, s))
+      states
+  end;
+  let rec explore_next nextstates seen numseen = function
+  | [] ->
+      List.rev nextstates
+  | (n, s, w) :: states ->
+      add_reducts nextstates seen numseen states n (do_step p prog ge time s w)
+
+  and add_reducts nextstates seen numseen states n = function
+  | [] ->
+      explore_next nextstates seen numseen states
+  | (r, s', w') :: reducts ->
+      let (n', nextstates', seen', numseen') =
+        try
+          (StateMap.find s' seen, nextstates, seen, numseen)
+        with Not_found ->
+          (numseen,
+           (numseen, s', w') :: nextstates,
+           StateMap.add s' numseen seen,
+           numseen + 1) in
+      if !trace >= 2 then begin
+        fprintf p "Transition state %d.%d --[%s]--> state %d.%d@."
+                  time n (camlstring_of_coqstring r) (time + 1) n'
+      end;
+      add_reducts nextstates' seen' numseen' states n reducts
+  in
+    let nextstates = explore_next [] StateMap.empty 1 states in
+    if nextstates <> [] then explore_all p prog ge (time + 1) nextstates
 
 (* The variant of the source program used to build the world for
    executing events.  
@@ -680,7 +647,6 @@ let execute prog =
       | Some(ge, s) ->
           match !mode with
           | First | Random ->
-              explore_one p prog1 ge 0 (s, world wge wm)
+              explore_one p prog1 ge 0 s (world wge wm)
           | All ->
-              explore_all p prog1 ge StateSet.empty 
-                                (PrioQueue.singleton (0, (s, world wge wm)))
+              explore_all p prog1 ge 0 [(1, s, world wge wm)]
diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
index 28d0cc8f..a75c95a5 100644
--- a/exportclight/Clightdefs.v
+++ b/exportclight/Clightdefs.v
@@ -23,6 +23,8 @@ Require Export AST.
 Require Export Ctypes.
 Require Export Cop.
 Require Export Clight.
+Require Import Maps.
+Require Import Errors.
 
 Definition tvoid := Tvoid.
 Definition tschar := Tint I8 Signed noattr.
@@ -50,9 +52,8 @@ Definition tattr (a: attr) (ty: type) :=
   | Tpointer elt _ => Tpointer elt a
   | Tarray elt sz _ => Tarray elt sz a
   | Tfunction args res cc => Tfunction args res cc
-  | Tstruct id fld _ => Tstruct id fld a
-  | Tunion id fld _ => Tunion id fld a
-  | Tcomp_ptr id _ => Tcomp_ptr id a
+  | Tstruct id _ => Tstruct id a
+  | Tunion id  _ => Tunion id a
   end.
 
 Definition tvolatile (ty: type) := tattr volatile_attr ty.
@@ -62,3 +63,9 @@ Definition talignas (n: N) (ty: type) :=
 
 Definition tvolatile_alignas (n: N) (ty: type) :=
   tattr {| attr_volatile := true; attr_alignas := Some n |} ty.
+
+Definition make_composite_env (comps: list composite_definition): composite_env :=
+  match build_composite_env comps with
+  | OK e => e
+  | Error _ => PTree.empty _
+  end.
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index 53eb96fd..c1009b4f 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -14,24 +14,45 @@
 (* *********************************************************************)
 
 open Printf
+open Commandline
 open Clflags
 
 (* Location of the compatibility library *)
 
-let stdlib_path = ref(
-  try
-    Sys.getenv "COMPCERT_LIBRARY"
-  with Not_found ->
-    Configuration.stdlib_path)
+let stdlib_path = ref Configuration.stdlib_path
+
+(* Invocation of external tools *)
 
-let command cmd =
+let command ?stdout args =
   if !option_v then begin
-    prerr_string "+ "; prerr_string cmd; prerr_endline ""
+    eprintf "+ %s" (String.concat " " args);
+    begin match stdout with
+    | None -> ()
+    | Some f -> eprintf " > %s" f
+    end;
+    prerr_endline ""
   end;
-  Sys.command cmd
-
-let quote_options opts =
-  String.concat " " (List.rev_map Filename.quote opts)
+  let argv = Array.of_list args in
+  assert (Array.length argv > 0);
+  try
+    let fd_out =
+      match stdout with
+      | None -> Unix.stdout
+      | Some f ->
+          Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in
+    let pid =
+      Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in
+    let (_, status) =
+      Unix.waitpid [] pid in
+    if stdout <> None then Unix.close fd_out;
+    match status with
+    | Unix.WEXITED rc -> rc
+    | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+        eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
+  with Unix.Unix_error(err, fn, param) ->
+    eprintf "Error executing '%s': %s: %s %s\n"
+            argv.(0) fn (Unix.error_message err) param;
+    -1
 
 let safe_remove file =
   try Sys.remove file with Sys_error _ -> ()
@@ -47,20 +68,32 @@ let print_error oc msg =
     List.iter print_one_error msg;
     output_char oc '\n'
 
+(* Determine names for output files.  We use -o option if specified
+   and if this is the final destination file (not a dump file).
+   Otherwise, we generate a file in the current directory. *)
+
+let output_filename ?(final = false) source_file source_suffix output_suffix =
+  match !option_o with
+  | Some file when final -> file
+  | _ -> 
+    Filename.basename (Filename.chop_suffix source_file source_suffix)
+    ^ output_suffix
+
 (* From C to preprocessed C *)
 
 let preprocess ifile ofile =
   let output =
-    if ofile = "-" then "" else sprintf "> %s" ofile in
-  let cmd =
-    sprintf "%s -D__COMPCERT__ %s %s %s %s"
-      Configuration.prepro
-      (if Configuration.has_runtime_lib
-       then sprintf "-I%s" !stdlib_path
-       else "")
-      (quote_options !prepro_options)
-      ifile output in
-  if command cmd <> 0 then begin
+    if ofile = "-" then None else Some ofile in
+  let cmd = List.concat [
+    Configuration.prepro;
+    ["-D__COMPCERT__"];
+    (if Configuration.has_runtime_lib
+     then ["-I" ^ !stdlib_path]
+     else []);
+    List.rev !prepro_options;
+    [ifile]
+  ] in
+  if command ?stdout:output cmd <> 0 then begin
     if ofile <> "-" then safe_remove ofile;
     eprintf "Error during preprocessing.\n";
     exit 2
@@ -82,24 +115,22 @@ let parse_c_file sourcename ifile =
     match Parse.preprocessed_file simplifs sourcename ifile with
     | None -> exit 2
     | Some p -> p in
-  (* Remove preprocessed file (always a temp file) *)
-  safe_remove ifile;
   (* Save C AST if requested *)
   if !option_dparse then begin
-    let ofile = Filename.chop_suffix sourcename ".c" ^ ".parsed.c" in
+    let ofile = output_filename sourcename ".c" ".parsed.c" in
     let oc = open_out ofile in
     Cprint.program (Format.formatter_of_out_channel oc) ast;
     close_out oc
   end;
   (* Conversion to Csyntax *)
   let csyntax =
-    match C2C.convertProgram ast with
+    match Timing.time "CompCert C generation" C2C.convertProgram ast with
     | None -> exit 2
     | Some p -> p in
   flush stderr;
   (* Save CompCert C AST if requested *)
   if !option_dcmedium then begin
-    let ofile = Filename.chop_suffix sourcename ".c" ^ ".compcert.c" in
+    let ofile = output_filename sourcename ".c" ".compcert.c" in
     let oc = open_out ofile in
     PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
     close_out oc
@@ -157,59 +188,6 @@ let explode_comma_option s =
   | [] -> assert false
   | hd :: tl -> tl
 
-type action =
-  | Set of bool ref
-  | Unset of bool ref
-  | Self of (string -> unit)
-  | String of (string -> unit)
-  | Integer of (int -> unit)
-
-let rec find_action s = function
-  | [] -> None
-  | (re, act) :: rem ->
-      if Str.string_match re s 0 then Some act else find_action s rem
-
-let parse_cmdline spec usage =
-  let acts = List.map (fun (pat, act) -> (Str.regexp pat, act)) spec in
-  let error () =
-    eprintf "%s" usage;
-    exit 2 in
-  let rec parse i =
-    if i < Array.length Sys.argv then begin
-      let s = Sys.argv.(i) in
-      match find_action s acts with
-      | None ->
-          if s <> "-help" && s <> "--help" 
-          then eprintf "Unknown argument `%s'\n" s;
-          error ()
-      | Some(Set r) ->
-          r := true; parse (i+1)
-      | Some(Unset r) ->
-          r := false; parse (i+1)
-      | Some(Self fn) ->
-          fn s; parse (i+1)
-      | Some(String fn) ->
-          if i + 1 < Array.length Sys.argv then begin
-            fn Sys.argv.(i+1); parse (i+2)
-          end else begin
-            eprintf "Option `%s' expects an argument\n" s; error()
-          end
-      | Some(Integer fn) ->
-          if i + 1 < Array.length Sys.argv then begin
-            let n =
-              try
-                int_of_string Sys.argv.(i+1)
-              with Failure _ ->
-                eprintf "Argument to option `%s' must be an integer\n" s;
-                error()
-            in
-            fn n; parse (i+2)
-          end else begin
-            eprintf "Option `%s' expects an argument\n" s; error()
-          end
-    end
-  in parse 1
-
 let usage_string =
 "The CompCert Clight generator
 Usage: clightgen [options] <source files>
@@ -238,36 +216,63 @@ General options:
   -v             Print external commands before invoking them
 "
 
+let print_usage_and_exit _ =
+  printf "%s" usage_string; exit 0
+
 let language_support_options = [
   option_fbitfields; option_flongdouble;
-  option_fstruct_return; option_fvararg_calls; option_fpacked_structs
+  option_fstruct_return; option_fvararg_calls; option_funprototyped;
+  option_fpacked_structs; option_finline_asm
 ]
 
+let set_all opts = List.iter (fun r -> r := true) opts
+let unset_all opts = List.iter (fun r -> r := false) opts
+
 let cmdline_actions =
   let f_opt name ref =
-    ["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in
+    [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in
   [
-  "-I$", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
-  "-D$", String(fun s -> prepro_options := s :: "-D" :: !prepro_options);
-  "-U$", String(fun s -> prepro_options := s :: "-U" :: !prepro_options);
-  "-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options);
-  "-dparse$", Set option_dparse;
-  "-dc$", Set option_dcmedium;
-  "-dclight$", Set option_dclight;
-  "-E$", Set option_E;
-  ".*\\.c$", Self (fun s -> process_c_file s);
-  "-Wp,", Self (fun s ->
-      prepro_options := List.rev_append (explode_comma_option s) !prepro_options);
-  "-fall$", Self (fun _ ->
-              List.iter (fun r -> r := true) language_support_options);
-  "-fnone$", Self (fun _ ->
-              List.iter (fun r -> r := false) language_support_options);
+(* Getting help *)
+  Exact "-help", Self print_usage_and_exit;
+  Exact "--help", Self print_usage_and_exit;
+(* Processing options *)
+  Exact "-E", Set option_E;
+(* Preprocessing options *)
+  Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
+  Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options);
+  Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options);
+  Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options);
+  Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options);
+  Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options);
+  Prefix "-Wp,", Self (fun s ->
+    prepro_options := List.rev_append (explode_comma_option s) !prepro_options);
+(* Language support options -- more below *)
+  Exact "-fall", Self (fun _ -> set_all language_support_options);
+  Exact "-fnone", Self (fun _ -> unset_all language_support_options);
+(* Tracing options *)
+  Exact "-dparse", Set option_dparse;
+  Exact "-dc", Set option_dcmedium;
+  Exact "-dclight", Set option_dclight;
+(* General options *) 
+  Exact "-v", Set option_v;
+  Exact "-stdlib", String(fun s -> stdlib_path := s);
   ]
+(* -f options: come in -f and -fno- variants *)
+(* Language support options *)
   @ f_opt "longdouble" option_flongdouble
   @ f_opt "struct-return" option_fstruct_return
   @ f_opt "bitfields" option_fbitfields
   @ f_opt "vararg-calls" option_fvararg_calls
+  @ f_opt "unprototyped" option_funprototyped
   @ f_opt "packed-structs" option_fpacked_structs
+  @ f_opt "inline-asm" option_finline_asm
+  @ [
+(* Catch options that are not handled *)
+  Prefix "-", Self (fun s ->
+      eprintf "Unknown option `%s'\n" s; exit 2);
+(* File arguments *)
+  Suffix ".c", Self (fun s -> process_c_file s);
+  ]
 
 let _ =
   Gc.set { (Gc.get()) with
@@ -284,4 +289,5 @@ let _ =
     end;
   Builtins.set C2C.builtins;
   CPragmas.initialize();
-  parse_cmdline cmdline_actions usage_string
+  parse_cmdline cmdline_actions
+
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index e4d1ce53..51dd0757 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -132,9 +132,20 @@ let coqfloat p n =
 let coqsingle p n =
   fprintf p "(Float32.of_bits %a)" coqint (Floats.Float32.to_bits n)
 
-(* Types *)
+let coqN p n =
+  fprintf p "%ld%%N" (N.to_int32 n)
+
+(* Raw attributes *)
 
-let use_struct_names = ref true
+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
+
+(* Types *)
 
 let rec typ p t =
   match attr_of_type t with
@@ -143,9 +154,9 @@ let rec typ p t =
   | { attr_volatile = true; attr_alignas = None} ->
         fprintf p "(tvolatile %a)" rtyp t
   | { attr_volatile = false; attr_alignas = Some n} ->
-        fprintf p "(talignas %ld%%N %a)" (N.to_int32 n) rtyp t
+        fprintf p "(talignas %a %a)" coqN n rtyp t
   | { attr_volatile = true; attr_alignas = Some n} ->
-        fprintf p "(tvolatile_alignas %ld%%N %a)" (N.to_int32 n) rtyp t
+        fprintf p "(tvolatile_alignas %a %a)" coqN n rtyp t
 
 and rtyp p = function
   | Tvoid -> fprintf p "tvoid"
@@ -176,16 +187,10 @@ and rtyp p = function
   | Tfunction(targs, tres, cc) ->
       fprintf p "@[<hov 2>(Tfunction@ %a@ %a@ %a)@]"
                 typlist targs typ tres callconv cc
-  | Tstruct(id, flds, _) ->
-      if !use_struct_names
-      then fprintf p "t%a" ident id
-      else fprintf p "@[<hov 2>(Tstruct %a@ %a@ noattr)@]" ident id fieldlist flds
-  | Tunion(id, flds, _) ->
-      if !use_struct_names
-      then fprintf p "t%a" ident id
-      else fprintf p "@[<hov 2>(Tunion %a@ %a@ noattr)@]" ident id fieldlist flds
-  | Tcomp_ptr(id, _) ->
-      fprintf p "(Tcomp_ptr %a noattr)" ident id
+  | Tstruct(id, _) ->
+      fprintf p "(Tstruct %a noattr)" ident id
+  | Tunion(id, _) ->
+      fprintf p "(Tunion %a noattr)" ident id
 
 and typlist p = function
   | Tnil ->
@@ -193,12 +198,6 @@ and typlist p = function
   | Tcons(t, tl) ->
       fprintf p "@[<hov 2>(Tcons@ %a@ %a)@]" typ t typlist tl
 
-and fieldlist p = function
-  | Fnil ->
-      fprintf p "Fnil"
-  | Fcons(id, t, fl) ->
-      fprintf p "@[<hov 2>(Fcons %a@ %a@ %a)@]" ident id typ t fieldlist fl
-
 and callconv p cc =
   if cc = cc_default
   then fprintf p "cc_default"
@@ -323,6 +322,10 @@ let rec expr p = function
          (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 *)
 
@@ -420,115 +423,14 @@ let print_ident_globdef p = function
   | (id, Gvar v) ->
       fprintf p "(%a, Gvar v_%s)" ident id (extern_atom id)
 
-(* Collecting the names and fields of structs and unions *)
-
-module TypeSet = Set.Make(struct
-  type t = coq_type
-  let compare = Pervasives.compare
-end)
-
-let struct_unions = ref TypeSet.empty
-
-let register_struct_union ty =
-  struct_unions := TypeSet.add ty !struct_unions
-
-let rec collect_type = function
-  | Tvoid -> ()
-  | Tint _ -> ()
-  | Tlong _ -> ()
-  | Tfloat _ -> ()
-  | Tpointer(t, _) -> collect_type t
-  | Tarray(t, _, _) -> collect_type t
-  | Tfunction(args, res, _) -> collect_type_list args; collect_type res
-  | Tstruct(id, fld, _) ->
-      register_struct_union (Tstruct(id, fld, noattr)) (*; collect_fields fld*)
-  | Tunion(id, fld, _) ->
-      register_struct_union (Tunion(id, fld, noattr)) (*; collect_fields fld*)
-  | Tcomp_ptr _ -> ()
-
-and collect_type_list = function
-  | Tnil -> ()
-  | Tcons(hd, tl) -> collect_type hd; collect_type_list tl
-
-and collect_fields = function
-  | Fnil -> ()
-  | Fcons(id, hd, tl) -> collect_type hd; collect_fields tl
-
-let rec collect_expr e =
-  collect_type (typeof e);
-  match e with
-  | Econst_int _ -> ()
-  | Econst_float _ -> ()
-  | Econst_long _ -> ()
-  | Econst_single _ -> ()
-  | Evar _ -> ()
-  | Etempvar _ -> ()
-  | Ederef(r, _) -> collect_expr r
-  | Efield(l, _, _) -> collect_expr l
-  | Eaddrof(l, _) -> collect_expr l
-  | Eunop(_, r, _) -> collect_expr r
-  | Ebinop(_, r1, r2, _) -> collect_expr r1; collect_expr r2
-  | Ecast(r, _) -> collect_expr r
-
-let rec collect_exprlist = function
-  | [] -> ()
-  | r1 :: rl -> collect_expr r1; collect_exprlist rl
-
-let rec temp_of_expr = function
-  | Etempvar(tmp, _) -> Some tmp
-  | Ecast(e, _) -> temp_of_expr e
-  | _ -> None
+(* Composite definitions *)
 
-let rec collect_stmt = function
-  | Sskip -> ()
-  | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
-  | Sset(id, e2) ->
-      begin match temp_of_expr e2 with
-      | Some tmp -> name_temporary tmp id
-      | None -> ()
-      end;
-      collect_expr e2
-  | Scall(optid, e1, el) -> collect_expr e1; collect_exprlist el
-  | Sbuiltin(optid, ef, tyl, el) -> collect_exprlist el
-  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
-  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
-  | Sloop(s1, s2) -> collect_stmt s1; collect_stmt s2
-  | Sbreak -> ()
-  | Scontinue -> ()
-  | Sswitch(e, cases) -> collect_expr e; collect_cases cases
-  | Sreturn None -> ()
-  | Sreturn (Some e) -> collect_expr e
-  | Slabel(lbl, s) -> collect_stmt s
-  | Sgoto lbl -> ()
-
-and collect_cases = function
-  | LSnil -> ()
-  | LScons(lbl, s, rem) -> collect_stmt s; collect_cases rem
-
-let collect_function f =
-  collect_type f.fn_return;
-  List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
-  List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
-  List.iter (fun (id, ty) -> collect_type ty) f.fn_temps;
-  collect_stmt f.fn_body
-
-let collect_globdef (id, gd) =
-  match gd with
-  | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res
-  | Gfun(Internal f) -> collect_function f
-  | Gvar v -> collect_type v.gvar_info
-
-let define_struct p ty =
-  match ty with
-  | Tstruct(id, _, _) | Tunion(id, _, _) ->
-      fprintf p "@[<hv 2>Definition t%a :=@  %a.@]@ " ident id typ ty
-  | _ -> assert false
-
-let define_structs p prog =
-  use_struct_names := false;
-  TypeSet.iter (define_struct p) !struct_unions;
-  use_struct_names := true;
-  fprintf p "@ "
+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_pair ident typ)) m
+    attribute a
 
 (* Assertion processing *)
 
@@ -605,14 +507,18 @@ let print_program p prog =
   fprintf p "%s" prologue;
   Hashtbl.clear temp_names;
   all_temp_names := StringSet.empty;
-  struct_unions := TypeSet.empty;
-  List.iter collect_globdef prog.prog_defs;
   define_idents p;
-  define_structs p prog;
   List.iter (print_globdef p) prog.prog_defs;
+  fprintf p "Definition composites : list composite_definition :=@ ";
+  print_list print_composite_definition p prog.prog_types;
+  fprintf p ".@ @ ";
   fprintf p "Definition prog : Clight.program := {|@ ";
   fprintf p "prog_defs :=@ %a;@ " (print_list print_ident_globdef) prog.prog_defs;
-  fprintf p "prog_main := %a@ " ident prog.prog_main;
+  fprintf p "prog_public :=@ %a;@ " (print_list ident) prog.prog_public;
+  fprintf p "prog_main := %a;@ " ident prog.prog_main;
+  fprintf p "prog_types := composites;@ ";
+  fprintf p "prog_comp_env := make_composite_env composites;@ ";
+  fprintf p "prog_comp_env_eq := refl_equal _@ ";
   fprintf p "|}.@ ";
   print_assertions p;
   fprintf p "@]@."
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index c77347da..eba416e4 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -81,7 +81,7 @@ module Cygwin_System =
        fprintf oc "_%s" s
 
     let symbol oc symb =
-      fprintf oc "%s" (extern_atom symb)
+      raw_symbol oc (extern_atom symb)
 
     let label oc lbl =
        fprintf oc "L%d" lbl
@@ -130,9 +130,9 @@ module ELF_System =
     
     let raw_symbol oc s =
       fprintf oc "%s" s
-  
-    let symbol oc symb =
-      fprintf oc "%s" (extern_atom symb)
+
+   let symbol oc symb =
+      raw_symbol oc (extern_atom symb)
 
     let label oc lbl =
       fprintf oc ".L%d" lbl
@@ -188,7 +188,7 @@ module MacOS_System =
      fprintf oc "_%s" s
 
     let symbol oc symb =
-      fprintf oc "_%s" (extern_atom symb)
+      raw_symbol oc (extern_atom symb)
 
     let label oc lbl =
       fprintf oc "L%d" lbl
@@ -1035,20 +1035,12 @@ let print_globdef oc (name, gdef) =
   | Gvar v -> print_var oc name v
 end)
 
-type target = ELF | MacOS | Cygwin
-
 let print_program oc p =
-  let target =   
-    match Configuration.system with
-    | "macosx" -> MacOS
-    | "linux"  -> ELF
-    | "bsd"    -> ELF
-    | "cygwin" -> Cygwin
-    | _        -> invalid_arg ("System " ^ Configuration.system ^ " not supported") in
-  let module Target = (val (match target with
-  | MacOS -> (module MacOS_System:SYSTEM)
-  | ELF -> (module ELF_System:SYSTEM)
-  | Cygwin -> (module Cygwin_System:SYSTEM)):SYSTEM) in
+  let module Target = (val (match  Configuration.system  with
+  | "macosx" -> (module MacOS_System:SYSTEM)
+  | "linux" | "bsd" -> (module ELF_System:SYSTEM)
+  | "cygwin" -> (module Cygwin_System:SYSTEM)
+  | _ ->  invalid_arg ("System " ^ Configuration.system ^ " not supported")):SYSTEM) in
   let module Printer = AsmPrinter(Target) in
   PrintAnnot.print_version_and_options oc Printer.comment;
   PrintAnnot.reset_filenames();
diff --git a/lib/Readconfig.mli b/lib/Readconfig.mli
new file mode 100644
index 00000000..c81e7786
--- /dev/null
+++ b/lib/Readconfig.mli
@@ -0,0 +1,39 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Reading configuration files *)
+
+(* The format of a configuration file is a list of lines
+      variable=value
+   The "value" on the right hand side is a list of whitespace-separated
+   words.  Quoting is honored with the same rules as POSIX shell:
+      \<newline>            for multi-line values
+      single quotes         no escapes within
+      double quotes         \$ \` \<doublequote> \\ \<newline> as escapes
+   Finally, lines starting with '#' are comments.
+*)
+
+val read_config_file: string -> unit
+  (** Read (key, value) pairs from the given file name.  Raise [Error]
+      if file is ill-formed. *)
+
+val key_val: string -> string list option
+  (** [key_val k] returns the value associated with key [k], if any.
+      Otherwise, [None] is returned. *)
+
+exception Error of string * int * string
+  (** Raised in case of error.
+      First argument is file name, second argument is line number,
+      third argument is an explanation of the error. *)
diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll
new file mode 100644
index 00000000..27ef32cf
--- /dev/null
+++ b/lib/Readconfig.mll
@@ -0,0 +1,111 @@
+{
+
+(* Recording key=val bindings *)
+
+let key_val_tbl : (string, string list) Hashtbl.t = Hashtbl.create 17
+
+let key_val key =
+  try Some(Hashtbl.find key_val_tbl key) with Not_found -> None
+
+(* Auxiliaries for parsing *)
+
+let buf = Buffer.create 32
+
+let stash inword words =
+  if inword then begin
+    let w = Buffer.contents buf in
+    Buffer.clear buf;
+    w :: words
+  end else
+    words
+
+(* Error reporting *)
+
+exception Error of string * int * string
+
+let error msg lexbuf =
+  Lexing.(raise (Error(lexbuf.lex_curr_p.pos_fname,
+                       lexbuf.lex_curr_p.pos_lnum,
+                       msg)))
+
+let ill_formed_line lexbuf = error "Ill-formed line" lexbuf 
+let unterminated_quote lexbuf = error "Unterminated quote" lexbuf
+let lone_backslash lexbuf = error "Lone \\ (backslash) at end of file" lexbuf
+
+}
+
+let whitespace = [' ' '\t' '\012' '\r']
+let newline = '\r'* '\n'
+let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']*
+
+rule begline = parse
+  | '#' [^ '\n']* ('\n' | eof)
+      { Lexing.new_line lexbuf; begline lexbuf }
+  | whitespace* (ident as key) whitespace* '=' 
+      { let words = unquoted false [] lexbuf in
+        Hashtbl.add key_val_tbl key (List.rev words);
+        begline lexbuf }
+  | eof
+      { () }
+  | _
+      { ill_formed_line lexbuf }
+
+and unquoted inword words = parse
+  | '\n' | eof    { Lexing.new_line lexbuf; stash inword words }
+  | whitespace+   { unquoted false (stash inword words) lexbuf }
+  | '\\' newline  { Lexing.new_line lexbuf; unquoted inword words lexbuf }
+  | '\\' (_ as c) { Buffer.add_char buf c; unquoted true words lexbuf }
+  | '\\' eof      { lone_backslash lexbuf }
+  | '\''          { singlequote lexbuf; unquoted true words lexbuf }
+  | '\"'          { doublequote lexbuf; unquoted true words lexbuf }
+  | _ as c        { Buffer.add_char buf c; unquoted true words lexbuf }
+
+and singlequote = parse
+  | eof           { unterminated_quote lexbuf }
+  | '\''          { () }
+  | newline       { Lexing.new_line lexbuf;
+                    Buffer.add_char buf '\n'; singlequote lexbuf }
+  | _ as c        { Buffer.add_char buf c; singlequote lexbuf }
+
+and doublequote = parse
+  | eof           { unterminated_quote lexbuf }
+  | '\"'          { () }
+  | '\\' newline  { Lexing.new_line lexbuf; doublequote lexbuf }
+  | '\\' (['$' '`' '\"' '\\'] as c)
+                  { Buffer.add_char buf c; doublequote lexbuf }
+  | newline       { Lexing.new_line lexbuf;
+                    Buffer.add_char buf '\n'; doublequote lexbuf }
+  | _ as c        { Buffer.add_char buf c; doublequote lexbuf }
+
+{
+
+(* The entry point *)
+
+let read_config_file filename =
+  let ic = open_in filename in
+  let lexbuf = Lexing.from_channel ic in
+  Lexing.(lexbuf.lex_start_p <- {lexbuf.lex_start_p with pos_fname = filename});
+  try
+    Hashtbl.clear key_val_tbl;
+    begline lexbuf;
+    close_in ic
+  with x ->
+    close_in ic; raise x
+
+(* Test harness *)
+(*
+open Printf
+
+let _ =
+  Hashtbl.clear key_val_tbl;
+  begline (Lexing.from_channel stdin);
+  Hashtbl.iter
+    (fun key value ->
+      printf "%s =" key;
+      List.iter (fun v -> printf " |%s|" v) value;
+      printf "\n")
+    key_val_tbl
+*)
+
+}
+
diff --git a/runtime/Makefile b/runtime/Makefile
index 1f0ccf25..9a872427 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -36,7 +36,7 @@ install:
 endif
 
 test/test_int64: test/test_int64.c $(LIB)
-	$(CC) -o $@ test/test_int64.c $(LIB)
+	$(CC) -g -o $@ test/test_int64.c $(LIB)
 
 clean::
 	rm -f test/test_int64
diff --git a/runtime/README b/runtime/README
new file mode 100644
index 00000000..5d824300
--- /dev/null
+++ b/runtime/README
@@ -0,0 +1,11 @@
+This is the support library for CompCert-generated code.
+It provides helper functions for:
+- 64-bit integer arithmetic
+- implementing the va_arg macro from <stdarg.h>
+
+The implementation is written in assembly language in the
+arm/ ia32/ powerpc/ directories.
+
+The c/ directory contains a C implementation of the 64-bit integer functions.
+It is provided for reference and as a guide for the asm implementations.
+
diff --git a/runtime/c/i64.h b/runtime/c/i64.h
new file mode 100644
index 00000000..dd584533
--- /dev/null
+++ b/runtime/c/i64.h
@@ -0,0 +1,43 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+extern unsigned long long __i64_shl(unsigned long long x, int amount);
+extern unsigned long long __i64_shr(unsigned long long x, int amount);
+extern signed long long __i64_sar(signed long long x, int amount);
+
+extern unsigned long long __i64_udivmod(unsigned long long n,
+                                        unsigned long long d,
+                                        unsigned long long * rp);
diff --git a/runtime/c/i64_dtos.c b/runtime/c/i64_dtos.c
new file mode 100644
index 00000000..d428e744
--- /dev/null
+++ b/runtime/c/i64_dtos.c
@@ -0,0 +1,74 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Conversion float64 -> signed int64 */
+
+long long __i64_dtos(double d)
+{
+  /* Extract bits of d's representation */
+  union { double d; unsigned long long i; } buf;
+  buf.d = d;
+  unsigned int h = buf.i >> 32;
+  /* Extract unbiased exponent */
+  int e = ((h & 0x7FF00000) >> 20) - (1023 + 52);
+  /* Check range of exponent */
+  if (e < -52) {
+    /* |d| is less than 1.0 */
+    return 0LL;
+  }
+  if (e >= 63 - 52) {
+    /* |d| is greater or equal to 2^63 */
+    if ((int) h < 0)
+      return -0x8000000000000000LL; /* min signed long long */
+    else
+      return  0x7FFFFFFFFFFFFFFFLL; /* max signed long long */
+  }
+  /* Extract true mantissa */
+  unsigned long long m =
+    (buf.i & ~0xFFF0000000000000LL) | 0x0010000000000000LL;
+  /* Shift it appropriately */
+  if (e >= 0)
+    m = __i64_shl(m, e);
+  else
+    m = __i64_shr(m, -e);
+  /* Apply sign to result */
+  if ((int) h < 0)
+    return -m;
+  else
+    return m;
+}
diff --git a/runtime/c/i64_dtou.c b/runtime/c/i64_dtou.c
new file mode 100644
index 00000000..c5f9df4d
--- /dev/null
+++ b/runtime/c/i64_dtou.c
@@ -0,0 +1,69 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Conversion float64 -> unsigned int64 */
+
+unsigned long long __i64_dtou(double d)
+{
+  /* Extract bits of d's representation */
+  union { double d; unsigned long long i; } buf;
+  buf.d = d;
+  unsigned int h = buf.i >> 32;
+  /* Negative FP numbers convert to 0 */
+  if ((int) h < 0) return 0ULL;
+  /* Extract unbiased exponent */
+  int e = ((h & 0x7FF00000) >> 20) - (1023 + 52);
+  /* Check range of exponent */
+  if (e < -52) {
+    /* d is less than 1.0 */
+    return 0ULL;
+  }
+  if (e >= 64 - 52) {
+    /* d is greater or equal to 2^64 */
+    return 0xFFFFFFFFFFFFFFFFULL; /* max unsigned long long */
+  }
+  /* Extract true mantissa */
+  unsigned long long m =
+    (buf.i & ~0xFFF0000000000000LL) | 0x0010000000000000LL;
+  /* Shift it appropriately */
+  if (e >= 0)
+    return __i64_shl(m, e);
+  else
+    return __i64_shr(m, -e);
+
+}
diff --git a/runtime/c/i64_sar.c b/runtime/c/i64_sar.c
new file mode 100644
index 00000000..a5f3364a
--- /dev/null
+++ b/runtime/c/i64_sar.c
@@ -0,0 +1,56 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Shift right signed */
+
+signed long long __i64_sar(signed long long x, int amount)
+{
+  unsigned xl = x;
+  int xh = x >> 32;
+  amount = amount & 63;
+  if (amount == 0) {
+    return x;
+  }
+  else if (amount < 32) {
+    unsigned rl = (xl >> amount) | (xh << (32 - amount));
+    int rh = xh >> amount;
+    return rl | ((signed long long) rh << 32);
+  } else {
+    return (signed long long) (xh >> (amount - 32));
+  }
+}
diff --git a/runtime/c/i64_sdiv.c b/runtime/c/i64_sdiv.c
new file mode 100644
index 00000000..3f21d9b7
--- /dev/null
+++ b/runtime/c/i64_sdiv.c
@@ -0,0 +1,51 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Signed division */
+
+signed long long __i64_sdiv(signed long long n, signed long long d)
+{
+  unsigned long long un, ud, uq, ur;
+  int nh = n >> 32, dh = d >> 32;
+  /* Take absolute values of n and d */
+  un = nh < 0 ? -n : n;
+  ud = dh < 0 ? -d : d;
+  uq = __i64_udivmod(un, ud, &ur);
+  /* Apply sign to quotient */
+  return (nh ^ dh) < 0 ? -uq : uq;
+}
diff --git a/runtime/c/i64_shl.c b/runtime/c/i64_shl.c
new file mode 100644
index 00000000..9b9aae57
--- /dev/null
+++ b/runtime/c/i64_shl.c
@@ -0,0 +1,55 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Shift left */
+
+unsigned long long __i64_shl(unsigned long long x, int amount)
+{
+  unsigned xl = x, xh = x >> 32;
+  amount = amount & 63;
+  if (amount == 0) {
+    return x;
+  }
+  else if (amount < 32) {
+    unsigned rl = xl << amount;
+    unsigned rh = (xh << amount) | (xl >> (32 - amount));
+    return rl | ((unsigned long long) rh << 32);
+  } else {
+    return ((unsigned long long) (xl << (amount - 32))) << 32;
+  }
+}
diff --git a/runtime/c/i64_shr.c b/runtime/c/i64_shr.c
new file mode 100644
index 00000000..c1db2a5f
--- /dev/null
+++ b/runtime/c/i64_shr.c
@@ -0,0 +1,55 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Shift right unsigned */
+
+unsigned long long __i64_shr(unsigned long long x, int amount)
+{
+  unsigned xl = x, xh = x >> 32;
+  amount = amount & 63;
+  if (amount == 0) {
+    return x;
+  }
+  else if (amount < 32) {
+    unsigned rl = (xl >> amount) | (xh << (32 - amount));
+    unsigned rh = xh >> amount;
+    return rl | ((unsigned long long) rh << 32);
+  } else {
+    return (unsigned long long) (xh >> (amount - 32));
+  }
+}
diff --git a/runtime/c/i64_smod.c b/runtime/c/i64_smod.c
new file mode 100644
index 00000000..ab15b6e6
--- /dev/null
+++ b/runtime/c/i64_smod.c
@@ -0,0 +1,51 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Signed remainder */
+
+signed long long __i64_smod(signed long long n, signed long long d)
+{
+  unsigned long long un, ud, ur;
+  int nh = n >> 32, dh = d >> 32;
+  /* Take absolute values of n and d */
+  un = nh < 0 ? -n : n;
+  ud = dh < 0 ? -d : d;
+  (void) __i64_udivmod(un, ud, &ur);
+  /* Apply sign to remainder */
+  return nh < 0 ? -ur : ur;
+}
diff --git a/runtime/c/i64_stod.c b/runtime/c/i64_stod.c
new file mode 100644
index 00000000..158b6892
--- /dev/null
+++ b/runtime/c/i64_stod.c
@@ -0,0 +1,46 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Conversion from signed int64 to float64 */
+
+double __i64_stod(signed long long x)
+{
+  unsigned xl = x;
+  signed xh = x >> 32;
+  return (double) xl + 0x1p+32 * (double) xh;
+}
diff --git a/runtime/c/i64_stof.c b/runtime/c/i64_stof.c
new file mode 100644
index 00000000..8410ba13
--- /dev/null
+++ b/runtime/c/i64_stof.c
@@ -0,0 +1,56 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Conversion from signed int64 to float32 */
+
+float __i64_stof(signed long long x)
+{
+  if (x < -(1LL << 53) || x >= (1LL << 53)) {
+    /* x is large enough that double rounding can occur.
+       Nudge x away from the points where double rounding occurs
+       (the "round to odd" technique) */
+    unsigned delta = ((unsigned) x & 0x7FF) + 0x7FF;
+    x = (x | delta) & ~0x7FFLL;
+  }
+  /* Convert to double */
+  unsigned xl = x;
+  signed xh = x >> 32;
+  double r = (double) xl + 0x1.0p32 * (double) xh;
+  /* Round to single */
+  return (float) r;
+}
diff --git a/runtime/c/i64_udiv.c b/runtime/c/i64_udiv.c
new file mode 100644
index 00000000..91fbf6e4
--- /dev/null
+++ b/runtime/c/i64_udiv.c
@@ -0,0 +1,45 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Unsigned division */
+
+unsigned long long __i64_udiv(unsigned long long n, unsigned long long d)
+{
+  unsigned long long r;
+  return __i64_udivmod(n, d, &r);
+}
diff --git a/runtime/c/i64_udivmod.c b/runtime/c/i64_udivmod.c
new file mode 100644
index 00000000..d8f5073a
--- /dev/null
+++ b/runtime/c/i64_udivmod.c
@@ -0,0 +1,158 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include <stddef.h>
+#include "i64.h"
+
+static unsigned __i64_udiv6432(unsigned u1, unsigned u0,
+                               unsigned v, unsigned *r);
+static int __i64_nlz(unsigned x);
+
+/* Unsigned division and remainder */
+
+unsigned long long __i64_udivmod(unsigned long long n,
+                                 unsigned long long d,
+                                 unsigned long long * rp)
+{
+  unsigned dh = d >> 32;
+  if (dh == 0) {
+    unsigned nh = n >> 32;
+    if (nh == 0) {
+      /* Special case 32 / 32 */
+      unsigned nl = n;
+      unsigned dl = d; 
+      *rp = (unsigned long long) (nl % dl);
+      return (unsigned long long) (nl / dl);
+    } else {
+      /* Special case 64 / 32 */
+      unsigned nl = n;
+      unsigned dl = d; 
+      unsigned qh = nh / dl;
+      unsigned rl;
+      unsigned ql = __i64_udiv6432(nh % dl, nl, dl, &rl);
+      *rp = (unsigned long long) rl; /* high word of remainder is 0 */
+      return ((unsigned long long) qh) << 32 | ql;
+    }
+  } else {
+    /* General case 64 / 64 */
+    unsigned dl = d;
+    /* Scale N and D down, giving N' and D' such that 2^31 <= D' < 2^32 */
+    int s = 32 - __i64_nlz(dh);  /* shift amount, between 1 and 32 */
+    unsigned long long np = __i64_shr(n, s);
+    unsigned dp = (unsigned) __i64_shr(d, s);
+    /* Divide N' by D' to get an approximate quotient Q */
+    unsigned q = __i64_udiv6432(np >> 32, np, dp, NULL);
+  again: ;
+    /* Tentative quotient Q is either correct or one too high */
+    /* Compute Q * D, checking for overflow */
+    unsigned long long p1 = (unsigned long long) dl * q;
+    unsigned long long p2 = (unsigned long long) (dh * q) << 32;
+    unsigned long long p = p1 + p2;
+    if (p < p1) {
+      /* Overflow occurred: adjust Q down by 1 and redo check */
+      q = q - 1; goto again;
+    }
+    /* Compute remainder R */
+    unsigned long long r = n - p;
+    if (n < p) {
+      /* Q is one too high, adjust Q down by 1 and R up by D */
+      q = q - 1; r = r + d;
+    }
+    *rp = r;
+    return (unsigned long long) q;
+  }
+}
+
+/* Unsigned division and remainder for 64 bits divided by 32 bits. */
+/* This is algorithm "divlu" from _Hacker's Delight_, fig 9.3 */
+
+static unsigned __i64_udiv6432(unsigned u1, unsigned u0,
+                               unsigned v, unsigned *r)
+{
+  const unsigned b = 65536; // Number base (16 bits).
+  unsigned un1, un0,        // Norm. dividend LSD's.
+           vn1, vn0,        // Norm. divisor digits.
+           q1, q0,          // Quotient digits.
+           un32, un21, un10,// Divided digit pairs.
+           rhat;            // A remainder.
+  int s;                    // Shift amount for norm.
+
+  if (u1 >= v) {            // If overflow,
+    if (r != NULL) *r = 0xFFFFFFFFU; // set rem to an impossible value,
+    return 0xFFFFFFFFU;              // and return largest possible quotient.
+  }
+  s = __i64_nlz(v);          // 0 <= s <= 31.
+  v = v << s;                // Normalize divisor.
+  vn1 = v >> 16;             // Break divisor up into
+  vn0 = v & 0xFFFF;          // two 16-bit digits.
+  un32 = (u1 << s) | ((u0 >> (32 - s)) & (-s >> 31));
+  un10 = u0 << s;            // Shift dividend left.
+  un1 = un10 >> 16;          // Break right half of
+  un0 = un10 & 0xFFFF;       // dividend into two digits.
+  q1 = un32/vn1;             // Compute the first quotient digit, q1.
+  rhat = un32 - q1*vn1;
+ again1:
+  if (q1 >= b || q1*vn0 > b*rhat + un1) {
+    q1 = q1 - 1;
+    rhat = rhat + vn1;
+    if (rhat < b) goto again1;
+  }
+  un21 = un32*b + un1 - q1*v; // Multiply and subtract.
+  q0 = un21/vn1;              // Compute the second quotient digit, q0
+  rhat = un21 - q0*vn1;
+again2:
+  if (q0 >= b || q0*vn0 > b*rhat + un0) {
+    q0 = q0 - 1;
+    rhat = rhat + vn1;
+    if (rhat < b) goto again2;
+  }
+  if (r != NULL) *r = (un21*b + un0 - q0*v) >> s;
+  return q1*b + q0;
+}
+
+/* Number of leading zeroes */
+
+static int __i64_nlz(unsigned x)
+{
+  if (x == 0) return 32;
+  int n = 0;
+  if (x <= 0x0000FFFF) { n += 16; x <<= 16; }
+  if (x <= 0x00FFFFFF) { n += 8; x <<= 8; }
+  if (x <= 0x0FFFFFFF) { n += 4; x <<= 4; }
+  if (x <= 0x3FFFFFFF) { n += 2; x <<= 2; }
+  if (x <= 0x7FFFFFFF) { n += 1; x <<= 1; }
+  return n;
+}
diff --git a/runtime/c/i64_umod.c b/runtime/c/i64_umod.c
new file mode 100644
index 00000000..d30e29c4
--- /dev/null
+++ b/runtime/c/i64_umod.c
@@ -0,0 +1,46 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Unsigned remainder */
+
+unsigned long long __i64_umod(unsigned long long n, unsigned long long d)
+{
+  unsigned long long r;
+  (void) __i64_udivmod(n, d, &r);
+  return r;
+}
diff --git a/runtime/c/i64_utod.c b/runtime/c/i64_utod.c
new file mode 100644
index 00000000..e70820a9
--- /dev/null
+++ b/runtime/c/i64_utod.c
@@ -0,0 +1,45 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Conversion from unsigned int64 to float64 */
+
+double __i64_utod(unsigned long long x)
+{
+  unsigned xl = x, xh = x >> 32;
+  return (double) xl + 0x1.0p32 * (double) xh;
+}
diff --git a/runtime/c/i64_utof.c b/runtime/c/i64_utof.c
new file mode 100644
index 00000000..87b85bfc
--- /dev/null
+++ b/runtime/c/i64_utof.c
@@ -0,0 +1,55 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+/* Conversion from unsigned int64 to float32 */
+
+float __i64_utof(unsigned long long x)
+{
+  if (x >= 1ULL << 53) {
+    /* x is large enough that double rounding can occur.
+       Nudge x away from the points where double rounding occurs
+       (the "round to odd" technique) */
+    unsigned delta = ((unsigned) x & 0x7FF) + 0x7FF;
+    x = (x | delta) & ~0x7FFULL;
+  }
+  /* Convert to double */
+  unsigned xl = x, xh = x >> 32;
+  double r = (double) xl + 0x1.0p32 * (double) xh;
+  /* Round to single */
+  return (float) r;
+}
diff --git a/runtime/test/test_int64.c b/runtime/test/test_int64.c
index ab7a231d..58a129b6 100644
--- a/runtime/test/test_int64.c
+++ b/runtime/test/test_int64.c
@@ -158,17 +158,21 @@ static void test1(u64 x, u64 y)
   u = __i64_stof(x);
   v = (float) (s64) x;
   if (u != v)
-    error++, printf("(double) %lld (s) = %a, expected %a\n", x, u, v);
+    error++, printf("(float) %lld (s) = %a, expected %a\n", x, u, v);
 
   f = (double) x;
-  z = __i64_dtou(f);
-  if (z != (u64) f)
-    error++, printf("(u64) %a = %llu, expected %llu\n", f, z, (u64) f);
+  if (f >= 0 && f < 0x1p+64) {
+    z = __i64_dtou(f);
+    if (z != (u64) f)
+      error++, printf("(u64) %a = %llu, expected %llu\n", f, z, (u64) f);
+  }
 
   f = (double) (s64) x;
-  t = __i64_dtos(f);
-  if (t != (s64) f)
-    error++, printf("(s64) %a = %lld, expected %lld\n", f, z, (s64) f);
+  if (f >= -0x1p+63 && f < 0x1p+63) {
+    t = __i64_dtos(f);
+    if (t != (s64) f)
+      error++, printf("(s64) %a = %lld, expected %lld\n", f, z, (s64) f);
+  }
 
   f = ((double) x) * 0.0001;
   z = __i64_dtou(f);