Recognize .i and .p source files as C sources not to be preprocessed.
Add CompCert version number and command line as comments in generated asm.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2407 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Updated for release 2.2.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2408 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Update for 2.2, continued

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Add option -Os to optimize for code size rather than for execution speed.
Refactored compilation flags that affect the Coq part (module Compopts).
Added support for C99 for loops with declarations.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Remove useless checks on type_of_global in dynamic semantics

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2411 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
PowerPC is big-endian, dammit.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2412 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Wrong type used for transforming lval = f(...)


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


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2414 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Updates for release 2.2

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2415 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
In Regalloc, dead code elimination, don't eliminate move operations
that pop the x87 FP stack (var <- FP0).  Otherwise, (void) f();
where f returns a float eventually produces a FP stack overflow.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2416 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Update clightgen for CompCert 2.2.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2417 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Silence the warning "Cannot build inversion information".


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2419 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Do not transform __builtin_va_arg for a struct or union type, this causes
an ugly error message in the back-end.  Rather, leave it as is, and let
C2C handle the error.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2422 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Force dependency of SelectOp on Compopts.


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

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2429 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
floatoflong_from_words, floatoflongu_from_words : proof of PowerPc implementation of long <-> float conversions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2430 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Use .comm to declare uninitialized BSS variables.  
To do: check for MacOS X, Cygwin, and also ARM.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2431 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Support array initialization lists that are too short

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2432 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Error messages were not displayed correctly if the main() function is missing or has the wrong type.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2433 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Type-checking of builtin volatile write Mfloat32 was too strict, causing type errors after optimization.


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