Merge branch 'named-structs'

- Switch CompCert C / Clight AST of composite types (structs and unions)
  from a structural representation to a nominal representation,
  closer to concrete syntax.
- This avoids algorithmic inefficiencies due to the structural representation.
- Closes PR#4.
- Smallstep: make small-step semantics more polymorphic in the type of the
  global environment.
- Globalenvs: introduce Senv.t (symbol environments) as a restricted view
  on Genv.t (full global environments).
- Events, Smallstep: use Senv instead of Genv to talk about global names.

1 files changed, 1 insertions, 1 deletions

diff --git a/driver/Driver.ml b/driver/Driver.ml
index b6224c32..5d4c2f9c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -108,7 +108,7 @@ let parse_c_file sourcename ifile =
   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;