| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
| |
More precise modeling of NaNs.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
which works better than the old one for the VST project.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2302 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2301 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
multiply-high and shifts.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
Delight).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2299 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2298 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
| |
- introduce Float.floatofint{,u} and use it in the semantics of C
- prove that it is equivalent to int->double conversion followed by
double->float rounding, and use this fact to justify code generation
in Cshmgen.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2294 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2293 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2292 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2291 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
casts int64 -> float64 -> float32. The latter causes double rounding
errors.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2290 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2289 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
test: add one test (2^64-1) / (2^32+3) to exercise a special case of
this long division.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2288 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
"struct" and "{", for compatibility with GCC.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2285 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2284 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2281 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2280 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2279 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2278 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2277 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Define type "block" as "positive" instead of "Z".
- Strengthen mem_unchanged_on so that the permissions are identical,
instead of possibly increasing.
- Move mem_unchanged_on from Events to Memory.Mem.
- Define it in terms of mem_contents rather than in terms of Mem.load.
- ExportClight: try to name temporaries introduced by SimplExpr
- SimplExpr: avoid reusing temporaries between different functions,
instead, thread a single generator through all functions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2270 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2263 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
PrintLTL: List.map -> List.rev_map
IRC: @ -> List.rev_append + don't maintain "extra" lists on precolored nodes.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2262 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
arm, ia32: reset table of file names at each run
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2261 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
- added RTL type "Tsingle"
- ABI-compatible passing of single-precision floats on ARM and x86
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
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
|