| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
| |
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@2253 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
|
| |
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
| |
Added options -falign-branch-targets and -falign-cond-branches (experimental).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2113 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
| |
cparser: add primitive support for enum types.
bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2061 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
|
|
| |
- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
| |
cparser: renamed Errors to Cerrors; removed packing into Cparser.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
| |
(definitely not semantics-preserving; hard to justify).
CPragmas: make sure SDAs are not recognized on MacOSX.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1836 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1832 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- native treatment of volatile accesses in CompCert C's semantics
- translation of volatile accesses to built-ins in SimplExpr
- native treatment of struct assignment and passing struct parameter by value
- only passing struct result by value remains emulated
- in cparser, remove emulations that are no longer used
- added C99's type _Bool and used it to express || and && more efficiently.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
| |
Added -flongdouble option (to turn long double into double)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1731 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
| |
test/*/Makefile: normalized 'bench' target
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1717 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
| |
test/regression: int main() so that interpretation works
Revised once more implementation of __builtin_memcpy (to check for PPC & ARM)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
| |
cparser: added experimental emulation of packed structs (PackedStruct.ml)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
|
|
| |
Added -dmach option and corresponding printer for Mach code.
CleanupLabelsproof.v: fixed for ARM
Driver.ml: -E sends output to stdout; support for .s and .S source files.
cparser/Elab.ml: spurious comment deleted.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1500 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Csyntax, Csem: source C language has side-effects within expressions,
performs implicit casts, and has nondeterministic reduction semantics
for expressions
- Cstrategy: deterministic red. sem. for the above
- Clight: the previous source C language, with pure expressions.
Added: temporary variables + implicit casts.
- New pass SimplExpr to pull side-effects out of expressions
(previously done in untrusted Caml code in cparser/)
- Csharpminor: added temporary variables to match Clight.
- Cminorgen: adapted, removed cast optimization (moved to back-end)
- CastOptim: RTL-level optimization of casts
- cparser: transformations Bitfields, StructByValue and StructAssign
now work on non-simplified expressions
- Added pretty-printers for several intermediate languages,
and matching -dxxx command-line flags.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1275 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
|
|
| |
#pragma use_section.
Some clean-ups in Cil2Csyntax.
Separate mach-dep parts of extraction/extraction.v into
<arch>/extractionMachdep.v
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
| |
to the Diab toolchain.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1165 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1163 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
Started to merge the ARM code generator.
Started to add support for PowerPC/EABI.
Use ocamlbuild to construct executable from Caml files.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
xleroy