aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* Pull request #192: improve the printing of Clight intermediate codeXavier Leroy2017-11-223-10/+29
* Added json export for the abstract ARM AssemblerBernhard Schommer2017-11-202-64/+338
* Moved arm eabi fixup to Asmexpand.Bernhard Schommer2017-11-163-159/+229
* New json printing interface.Bernhard Schommer2017-11-144-144/+208
* Remove no longer used function. Bug 22525Bernhard Schommer2017-11-105-8/+0
* Removed no longer used function. Bug 22525Bernhard Schommer2017-11-095-105/+1
* Use address for printing address constant. Bug 22525Bernhard Schommer2017-11-091-2/+3
* Generalize print_init.Bernhard Schommer2017-11-091-1/+40
* Fix jumptable issue.Bernhard Schommer2017-11-084-5/+8
* Simplifiy handling of constant emmitting.Bernhard Schommer2017-11-084-92/+71
* Remove superfluous function.Bernhard Schommer2017-11-066-11/+2
* Also quote \a.Bernhard Schommer2017-10-261-0/+2
* Fix register name of ais printing and moved label function up.Bernhard Schommer2017-10-251-4/+4
* Remove ais_annot_intval.Bernhard Schommer2017-10-241-13/+0
* Prefix ais annotations with location.Bernhard Schommer2017-10-241-2/+4
* Coq 8.7.0 supportXavier Leroy2017-10-202-3/+8
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-2015-3/+15
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-2015-3/+15
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-1931-66/+180
* | Check recursively for const for modifiable lvalues (#32)Bernhard Schommer2017-10-171-2/+15
* | Do not generate object files for linking.Bernhard Schommer2017-10-161-7/+14
* | Distinguish between long and int for cases.Bernhard Schommer2017-10-131-7/+7
* | Make the list unique. Bug 22239Bernhard Schommer2017-09-261-177/+22
* | Moved common buitlins to C2C gernic_builtins.Bernhard Schommer2017-09-265-34/+11
* | Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-09-250-0/+0
|\ \
| * | Remove coq warnings (#28)Bernhard Schommer2017-09-2272-638/+638
* | | Added dump-mnemonics option.Bernhard Schommer2017-09-258-2/+208
* | | Remove coq warnings (#28)Bernhard Schommer2017-09-2272-638/+638
|/ /
* | Disallow usage of default pattern for AsmToJSON.Bernhard Schommer2017-09-221-2/+11
* | Update version to 3.1Michael Schmidt2017-09-211-1/+1
* | Some lemmas.Bernhard Schommer2017-09-211-0/+14
* | Typo in Makefile: "ia32" is now "x86"Xavier Leroy2017-09-191-1/+1
* | 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