| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2258 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
(Ill-typed Clight/Cminor/RTL code was generated due to incorrect reuse
of destination temporary.)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2257 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
| |
with some static analysis tools).
*/PrintAsm.ml: don't cfa_adjust at Pfreeframe, as more code from the function can appear after (in case of tailcalls).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2256 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2255 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2254 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2251 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2249 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
compatibility in general and MacOS 10.8 standard includes in particular.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2248 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
Added corresponding test case.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2242 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
Improve dead code elimination for Xparmove.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2241 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
"the usual binary conversions" and be more robust towards future extensions
e.g. with 32-bit float values.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2239 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2238 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2237 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2236 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
| |
arm, powerpc: expand shifts inline in dtos and dtou
arm: branchless code for shl and shr
test: more tests for double -> long long conversions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2234 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2231 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
and the EABI.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2230 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2229 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
Simplified the scripts "coq" and "pg".
Updated deps.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2227 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2226 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2225 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2224 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2223 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2222 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2221 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2220 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2219 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2217 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
for compatibility with earlier CompCert versions.
But don't use them in PackedStructs.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2216 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2215 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2214 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
test/c: added SHA3
cfrontend: support casts between long long and pointers, and comparisons between them.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2213 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2212 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2211 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
Mint64.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2210 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2209 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
| |
Remove __builtin_{read,write}_reversed from IA32 and ARM ports.
Machregs: tighten destroyed_by_builtin
Packedstructs: use bswap if read/write-reversed not available.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2208 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2207 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2206 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2205 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2204 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2203 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2202 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2189 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|