index
:
debian-compcert
master
pristine-tar
upstream
Debian packaging for CompCert
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Alternate characterization of alignment constraints in memory injection, whic...
xleroy
2013-07-31
*
Update cchecklink w/ new Asm instructions Pmulh*
xleroy
2013-07-29
*
Optimize integer divisions by positive constants, turning them into
xleroy
2013-07-29
*
Add another expansion of shrx in terms of shifts and adds (from Hacker's Deli...
xleroy
2013-07-28
*
More properties about subtraction and borrow.
xleroy
2013-07-15
*
More accurate model of condition register flags for ARM and IA32.
xleroy
2013-07-13
*
Revised handling of int->float conversions:
xleroy
2013-07-08
*
Add option -no-runtime-lib.
xleroy
2013-07-08
*
Compile in debug mode and activate stack backtraces.
xleroy
2013-07-07
*
Bad printing of alignment on 'comm' symbols.
xleroy
2013-07-07
*
Treat casts int64 -> float32 as primitive operations instead of two
xleroy
2013-07-03
*
Follow-up to commit 2288: add test for special case of long division.
xleroy
2013-07-03
*
powerpc: faster implementation of long division modeled on that for IA32
xleroy
2013-07-03
*
Version 2.00 -> version 2.0
xleroy
2013-06-21
*
Recognize attribute((packed)) after a "struct {...}" and not just between "st...
xleroy
2013-06-21
*
Missing case for EF_inline_asm.
xleroy
2013-06-20
*
Updates in preparation for release 2.00
xleroy
2013-06-19
*
One more copyright header update.
xleroy
2013-06-17
*
Updating LICENSE and license headers, continued.
xleroy
2013-06-17
*
Update LICENSE file and headers for dual-licensed files.
xleroy
2013-06-17
*
Typo in comment
xleroy
2013-06-17
*
Update version number
xleroy
2013-06-16
*
Updated for release 2.00
xleroy
2013-06-16
*
Merge of the "princeton" branch:
xleroy
2013-06-16
*
More precise and faster recovery of function name from function or fundef value.
xleroy
2013-06-08
*
Fix compilation of runtime system.
xleroy
2013-05-29
*
Hunting stack overflows again:
xleroy
2013-05-27
*
powerpc: tentative support for Diab debug info
xleroy
2013-05-20
*
Merge of the float32 branch:
xleroy
2013-05-19
*
Prettier output
xleroy
2013-05-19
*
Issue with simplification of nested ?: expressions of different types.
xleroy
2013-05-19
*
Add option -fno-tailcalls to turn off tailcall elimination (causes problem wi...
xleroy
2013-05-17
*
Update PowerPC port
xleroy
2013-05-17
*
Update ARM port.
xleroy
2013-05-17
*
Preliminary support for debugging info (-g).
xleroy
2013-05-17
*
"->" can be applied to an array, not just a pointer.
xleroy
2013-05-16
*
MacOS: try to add link option -Wl,-no-pie when needed e.g. 10.8 and up.
xleroy
2013-05-13
*
Support __attribute__(ident) where ident is not bound. Useful for GCC compat...
xleroy
2013-05-13
*
Missing case: initialization of a global variable of type _Bool.
xleroy
2013-05-08
*
Add interferences at function entry with destroyed_at_function_entry.
xleroy
2013-05-08
*
Revised semantics and compilation of 2-argument C operators to better match
xleroy
2013-05-06
*
Refactoring: move definition of chunk_of_type to AST.v.
xleroy
2013-05-06
*
Syntax errors
xleroy
2013-05-06
*
Wrong pseudo-instr
xleroy
2013-05-06
*
Support for in64 -> float conversions w/ correct rounding.
xleroy
2013-05-06
*
ia32/i64_dtou: wrong play on rounding mode
xleroy
2013-05-05
*
Extend CSE of loads following stores to chunks Mint64 and Mfloat64al32.
xleroy
2013-05-02
*
Stack-align to 8 arguments of Tfloat and Tlong types, as per the SVR4 ABI and...
xleroy
2013-05-02
*
Clean up 'make clean'
xleroy
2013-05-01
*
Use "-as" to put CompCert modules in a compcert.xxx namespace.
xleroy
2013-05-01
[prev]
[next]