aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Trim blank linesv2.4xleroy2014-09-171-2/+0
* Update changelog and version for 2.4xleroy2014-09-172-3/+4
* Tolerance in parsing of 'section' pragmaxleroy2014-09-171-0/+3
* Cold feet: suppress builtins for load with reservation/store conditional, use...xleroy2014-08-285-47/+2
* Updatexleroy2014-08-281-1/+2
* Update for 2.4xleroy2014-08-271-23/+37
* Rename __builtin_cntlz to __builtin_clz.xleroy2014-08-2711-6/+25
* More efficient implementations of map, fold, etc.xleroy2014-08-271-164/+109
* More careful detection of inlined builtins. Produces better error messages i...xleroy2014-08-251-0/+1
* Use VFD regs to implement 64-bit mem-mem copies in builtin_memcpy_false.xleroy2014-08-213-5/+10
* Support C99 compound literals (by expansion in Unblock pass).xleroy2014-08-2116-454/+801
* Follow-up to commit 2613xleroy2014-08-201-0/+2
* Add builtins for load with reservation and conditional store.xleroy2014-08-205-1/+39
* Wrong types for strex builtins.xleroy2014-08-201-4/+4
* Better validation of target for ARMxleroy2014-08-201-1/+5
* Obvious typos in commit r2609xleroy2014-08-201-8/+8
* Add some more synchronization builtinsxleroy2014-08-202-1/+39
* Improve error reporting for unsupported compound literals.xleroy2014-08-201-1/+4
* Excessively strict validation: ofs + sz < modulus should have beenxleroy2014-08-201-4/+5
* Rename "-fthumb" option into "-mthumb" for GCC compatibility.xleroy2014-08-195-18/+22
* checklink/Check.ml: missing SDA addressing for store instructions.xleroy2014-08-195-14/+217
* Update dependenciesxleroy2014-08-191-14/+14
* powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.xleroy2014-08-187-124/+139
* Improve error detection and error messages for enums.xleroy2014-08-171-3/+7
* Issue with switch labels that are negative 32-bit integers.xleroy2014-08-172-4/+42
* Add some tests for "switch" over 32 and 64-bit integers.xleroy2014-08-173-1/+109
* - Support "switch" statements over 64-bit integersxleroy2014-08-1732-709/+1220
* Nicer reporting of I/O errors (e.g. "No such file").xleroy2014-08-131-23/+26
* Spurious error on a local static function declarationxleroy2014-08-131-0/+1
* Update commentxleroy2014-08-131-2/+1
* 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