aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
* Update Changelog for clightgenXavier Leroy2017-06-121-0/+1
* clightgen: add option -normalize to ensure that memory loads never occur "dee...Xavier Leroy2017-06-122-2/+177
* Merge pull request #185 from letouzey/no-BigNumPreludeXavier Leroy2017-06-071-1/+1
|\
| * Alphabet.v compiles even without the hints of BigNumPreludePierre Letouzey2017-06-061-1/+1
|/
* Early optimization of redundant *& and &* addressingsXavier Leroy2017-05-293-8/+59
* Merge pull request #184 from letouzey/zify-fixXavier Leroy2017-05-271-1/+1
|\
| * Inliningspec made compatible with a coming fix of zifyletouzey2017-05-271-1/+1
|/
* Issues with invalid x86 addressing modes (Github issue #183)Xavier Leroy2017-05-173-18/+27
* Make redefinition of composite a fatal error.Bernhard Schommer2017-05-091-2/+1
* Print 64bit constants for rldimn and rldimi.Bernhard Schommer2017-05-051-2/+2
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2017-05-051-2/+4
|\
| * Bring RISC-V port up to dateXavier Leroy2017-05-051-2/+4
* | bug 20956, print correct error message depending on architectureMichael Schmidt2017-05-031-2/+8
|/
* More asserts.Bernhard Schommer2017-05-031-1/+1
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-03107-1436/+3975
* Tunnelingproof: Remove assumption destroyed_by_cond c = nil.Xavier Leroy2017-05-021-66/+210
* RISC-V vararg.S: a "sw" instruction should be "sptr"Xavier Leroy2017-04-291-1/+1
* Update Changelog with recent changesXavier Leroy2017-04-281-1/+7
* RISC-V port and assorted changesXavier Leroy2017-04-2880-102/+12962
* Issue #179: clightgen produces wrong abstract syntax for "switch" statementsXavier Leroy2017-04-282-3/+11
* Always generate .merlin and _CoqProject files.Bernhard Schommer2017-04-281-19/+7
* Modest optimization of leaf functions (continued)Xavier Leroy2017-04-283-159/+116
* Modest optimization of leaf functionsXavier Leroy2017-04-284-46/+241
* Assert instead of unit.Bernhard Schommer2017-04-101-6/+6
* Filter out functions earlier. Bug 21343Bernhard Schommer2017-04-101-24/+27
* Fix name of function. Bug 21378Bernhard Schommer2017-04-071-1/+1
* Do not generate code for "inline definitions"Bernhard Schommer2017-04-073-30/+41
* Add optimization option finline.Bernhard Schommer2017-04-074-1/+8
* Another optimization of empty if/else and other useless conditional branchesXavier Leroy2017-04-062-31/+41
generated by cgit (git 2.34.1) at 2024-06-30 23:11:04 +0000