aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Expand)AuthorAgeFilesLines
...
* | Disallow usage of default pattern for AsmToJSON.Bernhard Schommer2017-09-221-2/+11
* | Fixed typo.Bernhard Schommer2017-08-241-1/+1
* | Added annot to json dump.Bernhard Schommer2017-07-241-3/+20
* | Print_annot should produce a string.Bernhard Schommer2017-07-191-5/+5
|/
* Constprop strength reduction (#17)Bernhard Schommer2017-07-123-16/+304
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-065-87/+179
* Issue #16P: wrong rlwinm instruction generated by constant propagationXavier Leroy2017-07-052-11/+26
* Adopted section names in AsmToJson.Bernhard Schommer2017-06-291-10/+23
* Formatted json printing.Bernhard Schommer2017-06-282-315/+307
* Added pseudo instruction for inline asm.Bernhard Schommer2017-06-201-0/+15
* Print 64bit constants for rldimn and rldimi.Bernhard Schommer2017-05-051-2/+2
* 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-0322-189/+2378
* RISC-V port and assorted changesXavier Leroy2017-04-282-0/+13
* Modest optimization of leaf functions (continued)Xavier Leroy2017-04-283-159/+116
* Modest optimization of leaf functionsXavier Leroy2017-04-283-44/+166
* 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-071-21/+23
* Replace 'decide equality' in powerpc/Op.v. Bug 21332Bernhard Schommer2017-04-031-4/+5
* Give explicit scopes to notations a#b and a##b and a#b<-cXavier Leroy2017-02-131-4/+6
* Use "Local" as prefixXavier Leroy2017-02-133-4/+4
* ARM, PowerPC: update Asmgenproof for Coq 8.6Xavier Leroy2017-02-131-6/+13
* Remove unused openBernhard Schommer2017-02-061-1/+0
* Added warning for inline asm in sdump. Bug 20593Bernhard Schommer2016-12-141-1/+6
* Use 64 bit address in debug information.Bernhard Schommer2016-11-101-0/+7
* Update PowerPC port (not tested yet)Xavier Leroy2016-10-251-2/+0
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-0115-296/+478
* Add interference for indirect calls.Bernhard Schommer2016-09-151-1/+5
* Merge branch 'master' of /common/repositories/git/tools/compcertBernhard Schommer2016-07-092-0/+32
|\
| * bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and __builtin_...Michael Schmidt2016-07-082-0/+32
* | Port to Coq 8.5pl2Xavier Leroy2016-07-081-3/+2
|/
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-212-3/+3
* fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert can...Michael Schmidt2016-06-071-1/+1
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-173-91/+122
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-273-268/+152
* */TargetPrinter.ml: wrong comment attached to Init_float32 constantsXavier Leroy2016-04-091-1/+1
* Reverted name for entry back to the old one.Bernhard Schommer2016-03-211-1/+1
* Merge branch 'master' into cleanupBernhard Schommer2016-03-213-61/+36
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-202-59/+34
| |\
| | * Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-58/+33
| | * Add support for EF_runtime externalsXavier Leroy2016-03-061-1/+1
| * | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-151-2/+2
| |/
* | Added interface for the Asmexpansion.Bernhard Schommer2016-03-161-4/+4
* | Change atom printer to use the common function.Bernhard Schommer2016-03-161-1/+1
* | Cleanup of AsmToJSON.Bernhard Schommer2016-03-163-126/+104
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-153-40/+40
* | Revert "Removed unused parameter from is_small/rel_data."Bernhard Schommer2016-03-155-23/+25
generated by cgit (git 2.34.1) at 2024-06-01 19:07:35 +0000