aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Reverted reintroduced quote of compilation dir.Bernhard Schommer2017-09-191-2/+2
* Deadcode: eliminate trivial Icond instructionsXavier Leroy2017-09-182-2/+9
* Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)Gergö Barany2017-09-189-21/+43
* Merge pull request #202 from gergo-/mla-foldingXavier Leroy2017-09-152-0/+102
|\
| * Strength reduction patterns for ARM mla instruction.Gergö Barany2017-09-152-0/+102
|/
* Update the Cygwin x86-32 portXavier Leroy2017-09-121-10/+11
* configure for x86-32/Cygwin: ignore __attribute__Xavier Leroy2017-09-111-1/+1
* Resurrect the Cygwin x86-32 portXavier Leroy2017-09-112-2/+60
* test/*/Makefile: suppress dependencies on ../../ccompXavier Leroy2017-09-112-6/+6
* Makefile: chmod a-w instead of chmod -wXavier Leroy2017-09-111-1/+1
* Issue #199: improve namespace management for clightgen-produced filesXavier Leroy2017-08-282-16/+6
* For running tests with the interpreter, use the correct -stdlib optionXavier Leroy2017-08-281-3/+2
* test/compression: use unique temporary files for testingXavier Leroy2017-08-271-7/+7
* riscV/Conventions1: in 32-bit mode, wrong size for stack-allocated arguments ...Xavier Leroy2017-08-261-2/+5
* riscV/Machregs: no printable name was associated to register X31Xavier Leroy2017-08-261-1/+1
* test/ : stop at first error in "make all"Xavier Leroy2017-08-261-1/+1
* test/: add a CCOMPOPTS make variable to pass additional compile-time flagsXavier Leroy2017-08-265-5/+5
* Reduce the running times of the tests in test/cXavier Leroy2017-08-2630-87/+75
* Prefixed runtime functions.Bernhard Schommer2017-08-2560-269/+269
* Document -finline in help.Bernhard Schommer2017-08-241-0/+1
* Fixed typo.Bernhard Schommer2017-08-241-1/+1
* Extended support for the nostartfiles option.Bernhard Schommer2017-08-231-6/+11
* ARM in Thumb mode: simpler instruction sequence for Pbtbl pseudo, continuedXavier Leroy2017-08-221-1/+2
* ARM in Thumb mode: simpler instruction sequence for Pbtbl pseudoXavier Leroy2017-08-222-6/+7
* Issue P #25: make sure sizeof(long double) = sizeof(double) in all contexts.Xavier Leroy2017-08-222-10/+12
* Update documentation index for release 3.1v3.1Xavier Leroy2017-08-181-23/+17
* Merge remote-tracking branch 'private/master'Xavier Leroy2017-08-188-91/+201
|\
| * Merge pull request #22 from AbsIntPrivate/arm_large_offsetsXavier Leroy2017-08-188-91/+201
| |\
| | * ARM: tweak stack layout so that back link and return address are lowerXavier Leroy2017-08-171-37/+34
| | * ARM port: replace Psavelr pseudo-instruction by actual instructionsXavier Leroy2017-08-176-47/+88
| | * Asmgenproof0: some more useful lemmasXavier Leroy2017-08-171-0/+29
| | * ARM: Generate Pcfi_rel_offset directives directly from AsmgenXavier Leroy2017-08-174-12/+17
| | * Push correct registerMichael Schmidt2017-08-021-1/+1
| | * Improve stack offset addressingMichael Schmidt2017-08-025-35/+73
* | | configure: Wording and formatting of the Skylake/OCaml warningXavier Leroy2017-08-181-2/+3
* | | Update Changelog in preparation for release 3.1Xavier Leroy2017-08-181-2/+8
|/ /
* / Issue #196: excessive proof-checking times in .v files generated by clightgenXavier Leroy2017-08-153-13/+34
|/
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2017-07-311-1/+3
|\
| * Mention rv32- and rv64- configurations in the help messageXavier Leroy2017-07-311-0/+2
| * Accept Coq version 8.6.1 as supportedXavier Leroy2017-07-311-1/+1
* | Warning for Skylake/Kabylake systems.Bernhard Schommer2017-07-311-0/+4
|/
* Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-07-271-20/+27
|\
| * use TMPDIR also for asm-cfi testMichael Schmidt2017-07-271-5/+5
| * generalize test for compiler optionsMichael Schmidt2017-07-271-15/+22
* | Update Changelog with news since release 3.0.1Xavier Leroy2017-07-271-4/+29
|/
* Integrated fixup code in estimated size.Bernhard Schommer2017-07-261-0/+3
* Added annot to json dump.Bernhard Schommer2017-07-241-3/+20
* Print_annot should produce a string.Bernhard Schommer2017-07-195-40/+54
* No verbose debug info in default mode.Bernhard Schommer2017-07-141-5/+17
* Update documentation entry point for release 3.0 (retroactively)Xavier Leroy2017-07-131-5/+8
generated by cgit (git 2.34.1) at 2024-06-29 01:24:02 +0000