| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2442 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
More precise classification of float results of arithmetic operations,
in preparation for future work on the C/Clight static type system.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2441 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
those defined in the function. Semantically, both are correct, but the latter may cause RTLtyping to fail if some regs are uninitialized and a collision occurs between regs of different types.
RTL: move the function resource computations there, as it could be useful for other passes some day.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2440 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
Elab: Handle C99 designated initializers.
C2C, Initializers: more precise intermediate AST for initializers.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
the new Lineartyping can't keep track of single floats that were spilled.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2438 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
Update Makefile and dependencies.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2436 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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 machine registers that contain
a single-precision float.
- Stackingproof: adapted accordingly.
This addresses a defect report by D. Dickman whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2435 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
type errors after optimization.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2434 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
missing or has the wrong type.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2433 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2432 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
implementation of long <-> float conversions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2430 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2429 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2428 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2419 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2417 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2415 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2414 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2413 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2412 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2411 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2408 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
| |
arguments.
Test sizeof1: adapt to the fact that alignof(double) is either 4 or 8 depending on platform.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2406 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2405 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2404 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
- Revised printing of intermediate RTL code.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
| |
- endianness
- alignment constraints for 8-byte types
(which is 4 for x86 ABI and 8 for other ABIs)
- NaN handling options (superceding the Nan module, removed).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2401 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2400 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
NeedOp, Deadcode: must have distinct needs per argument of an operator.
This change remains to be propagated to IA32 and PPC.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2398 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2397 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
arm: typo.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2396 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
ARM) or an array type (PowerPC).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2395 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
tested on PowerPC and ARM.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
(incomplete_type, sizeof, etc).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2393 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
__builtin_memcpy_aligned now supports the case sz = 0.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2392 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
Cutil.ml: fix sizeof calculation of structs.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2391 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
Additional warnings for empty initializer braces and zero-sized arrays.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2390 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
(option -funprototyped, on by default).
Error if call to vararg function and -fvararg-calls is off.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2389 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
PackedStructs.ml: remove "packed" attribute once processed.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2388 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
More informative "unsupported" error messages.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- C function types and Cminor signatures annotated by calling conventions.
esp. vararg / not vararg
- Cshmgen: generate correct code for function call where there are
more arguments than listed in the function prototype. This is
still undefined behavior according to the formal semantics,
but correct code is generated.
- C2C, */PrintAsm.ml: remove "printf$iif" hack.
- powerpc/, checklink/: don't generate stubs for variadic functions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
like we already do in ARM Asm.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|