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
*
powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.
xleroy
2014-08-18
*
Improve error detection and error messages for enums.
xleroy
2014-08-17
*
Issue with switch labels that are negative 32-bit integers.
xleroy
2014-08-17
*
Add some tests for "switch" over 32 and 64-bit integers.
xleroy
2014-08-17
*
- Support "switch" statements over 64-bit integers
xleroy
2014-08-17
*
Nicer reporting of I/O errors (e.g. "No such file").
xleroy
2014-08-13
*
Spurious error on a local static function declaration
xleroy
2014-08-13
*
Update comment
xleroy
2014-08-13
*
Add Mem.free_parallel_inject and use it to simplify Events a bit.
xleroy
2014-07-31
*
configure: distinguish between ABI and processor model.
xleroy
2014-07-29
*
All targets: add __builtin_membar
xleroy
2014-07-28
*
PowerPC port: refactored the expansion of built-in functions and
xleroy
2014-07-28
*
Updated Changelog
xleroy
2014-07-28
*
The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.
xleroy
2014-07-28
*
ARM port: add support for Thumb2. To be tested.
xleroy
2014-07-27
*
Update for single-precision floats. Calls to vararg functions remain
xleroy
2014-07-24
*
Add _a memory accesses.
xleroy
2014-07-23
*
Update with _a memory accesses
xleroy
2014-07-23
*
Simplify COQINCLUDES
xleroy
2014-07-23
*
Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.
xleroy
2014-07-23
*
Redundant -I in CAMLINCLUDES
xleroy
2014-07-23
*
Update "read_as_zeros" property.
xleroy
2014-07-23
*
Merge of "newspilling" branch:
xleroy
2014-07-23
*
Tweaks to support defunctorization.
xleroy
2014-07-23
*
Make Alphabet.v compatible with an environnment where Containers is installed
jjourdan
2014-07-04
*
Add Proof keyword so that documentation generation works
jjourdan
2014-07-04
*
Add "read_as_zero" property for memory areas initialized by Init_space.
xleroy
2014-06-30
*
Document commit r2507.
xleroy
2014-06-05
*
Cleaner, more resilient parsing of pragmas.
xleroy
2014-06-05
*
Instead of having two expansions of shrximm (one in SelectOp, one in Asmgen),...
xleroy
2014-05-28
*
Refactoring: move symbol_offset into Genv.
xleroy
2014-05-24
*
Empty declarations
jjourdan
2014-05-23
*
In enter_or_refine_ident: revised handling of "extern" decls.
xleroy
2014-05-18
*
Another corner case for string literal initializers: char * x[] = { "lit" }
xleroy
2014-05-18
*
Typo in struct_declaration_list causing conflicts.
xleroy
2014-05-18
*
Bump
xleroy
2014-05-15
*
- Re-added support for "__func__" identifier as per ISO C99.
xleroy
2014-05-15
*
Assorted fixes to fix parsing issues and be more GCC-like:
xleroy
2014-05-12
*
Incorrect conversion of K&R functions. Example of problem:
xleroy
2014-05-12
*
Fix string litteral parsing
jjourdan
2014-05-11
*
Bump
xleroy
2014-05-09
*
Fixed regression on initializers of the form T x[N] = "literal";
xleroy
2014-05-08
*
- Added alternate keywords __inline, __restrict, etc, for GCC compatibility
xleroy
2014-05-08
*
Update Coq documentation
xleroy
2014-05-05
*
Update for release 2.3.
xleroy
2014-05-05
*
Fused multiply-add for IA32.
xleroy
2014-05-05
*
Stern warning on non-prototype function definitions.
xleroy
2014-05-05
*
Do not allow typedef_name in identifier lists of K&R style definitions
jjourdan
2014-05-05
*
Support for old-style K&R function definitions.
xleroy
2014-05-05
*
Treat all identifiers as VAR_NAME by default (i.e. if not bound by a typedef)...
xleroy
2014-05-05
[next]