Merge of branch linear-typing:

1) Revised division of labor between RTLtyping and Lineartyping:
- RTLtyping no longer keeps track of single-precision floats,
  switches from subtype-based inference to unification-based inference.
- Unityping: new library for unification-based inference.
- Locations: don't normalize at assignment in a stack slot
- Allocation, Allocproof: simplify accordingly.
- Lineartyping: add inference of locations that contain
  a single-precision float.
- Stackingproof: adapted accordingly.

This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c).

This corresponds to commits 2435+2436 plus improvements in Lineartyping.

2) Add -dtimings option to measure compilation times.
Moved call to C parser from Elab to Parse, to make it easier to
measure parsing time independently of elaboration time.


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

1 files changed, 2 insertions, 5 deletions

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index e468ab2..0d2cb89 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2081,11 +2081,8 @@ let _ = elab_funbody_f := elab_funbody
 
 (** * Entry point *)
 
-let elab_preprocessed_file name ic =
-  let lb = Lexer.init name ic in
+let elab_file prog =
   reset();
-  ignore (elab_definitions false (Builtins.environment())
-                                 (Parser.file Lexer.initial lb));
-  Lexer.finish();
+  ignore (elab_definitions false (Builtins.environment()) prog);
   elaborated_program()