aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* | 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
* Constprop strength reduction (#17)Bernhard Schommer2017-07-124-16/+325
* SimlLocals.Sdebug_var: wrong type for 64-bit platformsXavier Leroy2017-07-091-1/+1
* Add a -ignore-coq-version flag to configure (continued)Xavier Leroy2017-07-061-2/+2
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-0618-99/+283
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-0629-37/+211
* Issue #16P: wrong rlwinm instruction generated by constant propagationXavier Leroy2017-07-053-13/+30
* Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-07-051-0/+30
|\
| * Merge pull request #14 from AbsIntPrivate/configure_no_pieMichael Schmidt2017-07-051-0/+30
| |\
| | * add check for -no-pie at configure-timeMichael Schmidt2017-07-041-0/+30
| |/
* | Add a -ignore-coq-version flag to configure (continued)Xavier Leroy2017-07-051-1/+1
* | Add a -ignore-coq-version flag to configureXavier Leroy2017-07-051-2/+10
|/
* Adopted section names in AsmToJson.Bernhard Schommer2017-06-291-10/+23
* Revert "Update git ignore spec"Bernhard Schommer2017-06-281-1/+0
* Merge branch 'master' of /common/repositories/git/tools/compcertBernhard Schommer2017-06-281-0/+1
|\
| * Update git ignore specMarkus Pister2017-06-281-0/+1
* | Formatted json printing.Bernhard Schommer2017-06-289-353/+370
|/
* Added a little bit more compilation info to sdump.Bernhard Schommer2017-06-263-4/+16
* Added pseudo instruction for inline asm.Bernhard Schommer2017-06-201-0/+15
generated by cgit (git 2.34.1) at 2024-06-29 14:47:47 +0000