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
Reducing compilation times: (by 35% on one example)
- Use a hashtable instead of an AVL set for adjSet
- Inlining and algebraic simplification of spillCost into selectSpill.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2450 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Support Onot operator / notl instruction.  More constant propagation during selection.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2451 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons over booleans.
Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31].
Driver: timer for whole compilation.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
ia32/Select*: complete the modifications to shifts.
Makefile: missing "clean" actions.
Makefile/pg/coq: honor $COQBIN if set (as suggested by P. Boutillier)
  to facilitate testing with different Coq versions.


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


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2454 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Use "incrdecr_type ty" instead of "typeconv ty" as the intermediate type
for Epostincr operations.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2455 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Continued: change typeconv t into incrdecr_type t for Epostincr.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2456 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Clean-up pass on C types:
- Ctypes: add useful functions on attributes; remove attrs in typeconv
    (because attributes are meaningless on r-values)
- C2C: fixed missing or redundant Evalof
- Cop: ignore attributes in ptr + int and ptr - int (meaningless on r-values);
    add sanity check between typeconv/classify_binarith and the C99 standard.
- cparser: fixed several cases where incorrect type annotations were put
    on expressions.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2457 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Update with post-2.2 changes

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2460 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Integration of Jacques-Henri Jourdan's verified parser.
(Merge of branch newparser.)


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Bump version number before I forget

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2470 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Check availability of tools

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2471 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Be less picky in the way we parse '#' lines

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2472 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Preliminary support for EABI-hardfloat calling conventions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2473 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
New sub-target: arm-hardfloat

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2474 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
ARM: honor common variables.
Changelog: update.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2475 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Adapt to the two different calling conventions for floats.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2476 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Treat all identifiers as VAR_NAME by default (i.e. if not bound by a typedef).  This produces better error messages for unbound variable names (proper error message in Elab rather than cryptic syntax error in pre_parser).


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2477 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Support for old-style K&R function definitions.


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