aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Add Mem.free_parallel_inject and use it to simplify Events a bit.xleroy2014-07-313-35/+50
* configure: distinguish between ABI and processor model.xleroy2014-07-2917-55/+116
* All targets: add __builtin_membarxleroy2014-07-285-29/+53
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-2820-1367/+1200
* Updated Changelogxleroy2014-07-281-0/+28
* The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.xleroy2014-07-284-76/+30
* ARM port: add support for Thumb2. To be tested.xleroy2014-07-2728-799/+1194
* Update for single-precision floats. Calls to vararg functions remainxleroy2014-07-245-32/+153
* Add _a memory accesses.xleroy2014-07-231-6/+6
* Update with _a memory accessesxleroy2014-07-231-2/+2
* Simplify COQINCLUDESxleroy2014-07-231-3/+2
* Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.xleroy2014-07-2313-730/+146
* Redundant -I in CAMLINCLUDESxleroy2014-07-231-2/+3
* Update "read_as_zeros" property.xleroy2014-07-231-1/+3
* Merge of "newspilling" branch:xleroy2014-07-23113-4267/+6831
* Tweaks to support defunctorization.xleroy2014-07-231-9/+19
* Make Alphabet.v compatible with an environnment where Containers is installedjjourdan2014-07-041-1/+1
* Add Proof keyword so that documentation generation worksjjourdan2014-07-041-0/+2
* Add "read_as_zero" property for memory areas initialized by Init_space.xleroy2014-06-301-14/+106
* Document commit r2507.xleroy2014-06-051-0/+3
* Cleaner, more resilient parsing of pragmas.xleroy2014-06-053-55/+103
* Instead of having two expansions of shrximm (one in SelectOp, one in Asmgen),...xleroy2014-05-284-78/+54
* Refactoring: move symbol_offset into Genv.xleroy2014-05-2424-218/+156
* Empty declarationsjjourdan2014-05-235-11181/+11253
* In enter_or_refine_ident: revised handling of "extern" decls.xleroy2014-05-181-29/+38
* Another corner case for string literal initializers: char * x[] = { "lit" }xleroy2014-05-183-1/+14
* Typo in struct_declaration_list causing conflicts.xleroy2014-05-181-1/+1
* Bumpv2.3pl2xleroy2014-05-151-1/+2
* - Re-added support for "__func__" identifier as per ISO C99.xleroy2014-05-157-5751/+5477
* Assorted fixes to fix parsing issues and be more GCC-like:xleroy2014-05-128-13541/+14068
* Incorrect conversion of K&R functions. Example of problem:xleroy2014-05-122-2/+10
* Fix string litteral parsingjjourdan2014-05-112-3/+7
* Bumpxleroy2014-05-091-1/+1
* Fixed regression on initializers of the form T x[N] = "literal";xleroy2014-05-084-8/+27
* - Added alternate keywords __inline, __restrict, etc, for GCC compatibilityxleroy2014-05-082-4/+24
* Update Coq documentationv2.3xleroy2014-05-052-4/+4
* Update for release 2.3.xleroy2014-05-052-2/+3
* Fused multiply-add for IA32.xleroy2014-05-054-4/+45
* Stern warning on non-prototype function definitions.xleroy2014-05-051-0/+1
* Do not allow typedef_name in identifier lists of K&R style definitionsjjourdan2014-05-051-4/+4
* Support for old-style K&R function definitions.xleroy2014-05-056-4545/+5621
* Treat all identifiers as VAR_NAME by default (i.e. if not bound by a typedef)...xleroy2014-05-052-15/+8
* Adapt to the two different calling conventions for floats.xleroy2014-05-026-0/+14
* ARM: honor common variables.xleroy2014-05-022-12/+27
* New sub-target: arm-hardfloatxleroy2014-05-021-0/+11
* Preliminary support for EABI-hardfloat calling conventionsxleroy2014-05-023-48/+938
* Be less picky in the way we parse '#' linesxleroy2014-05-021-11/+23
* Check availability of toolsxleroy2014-05-021-0/+50
* Bump version number before I forgetxleroy2014-05-011-1/+1
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-2949-3224/+66259
generated by cgit (git 2.34.1) at 2024-07-01 23:44:32 +0000