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