Assorted changes to reduce stack and heap requirements when compiling very big functions.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
More aggressive CSE across Ibuiltin.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2152 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Remove the C primitives for unsigned long long arithmetic, replaced
by pure OCaml code.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2153 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a limitation in the a3 analyzers.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2154 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diab asm syntax issue

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2155 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Update clightgen to changes in Camlcoq and in AST.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2156 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
RTLtyping: now performed entirely in Coq, no need for an external Caml oracle + a validator.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2157 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Watch out for behaviors exponential in the nesting of struct/union types. 


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Better locations for error messages relative to type specifiers.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2159 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Error when calling un-prototyped function.
Removed warning "un-prototyped function type", fires too often.  The important thing is to mark errors when declaring and calling unproto fns.


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

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2164 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
List.iteri not in OCaml < 4.00, better not use it.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Updated issues with coqchk.  See PR#3026 on the Coq bug tracker.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2189 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Big merge of the newregalloc-int64 branch.  Lots of changes in two directions:
1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Interp.ml: support printf of long long
test/regression: add test "int32"; update test "int64"


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2201 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Tests "floats" and "floats-basics" moved from test/c to test/regression


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2202 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Added FFTW benchmark provided by Guillaume Melquiond


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2203 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Remove __i64_{neg,add,sub,mul}, now handled directly by the compiler.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2204 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Configuring the assembler used for the runtime lib

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2205 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Split arch/int64.s into one file per function.


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