aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Expand)AuthorAgeFilesLines
* Add missing tab character, bug 23541Michael Schmidt2018-05-021-1/+1
* Add new powerpc builtins.Michael Schmidt2018-04-275-4/+44
* Print symbols as symbols.Bernhard Schommer2018-03-081-16/+19
* Use binary output.Bernhard Schommer2018-03-071-1/+1
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-061-9/+10
* Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)Xavier Leroy2018-02-162-6/+55
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-1/+1
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-052-5/+17
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-051-0/+3
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-052-6/+13
* New json printing interface.Bernhard Schommer2017-11-141-143/+18
* Remove no longer used function. Bug 22525Bernhard Schommer2017-11-101-2/+0
* Removed no longer used function. Bug 22525Bernhard Schommer2017-11-091-30/+0
* Fix jumptable issue.Bernhard Schommer2017-11-081-1/+1
* Simplifiy handling of constant emmitting.Bernhard Schommer2017-11-081-20/+14
* Remove superfluous function.Bernhard Schommer2017-11-061-2/+0
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-201-0/+1
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-201-0/+1
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-194-13/+29
* | Make the list unique. Bug 22239Bernhard Schommer2017-09-261-177/+22
* | Moved common buitlins to C2C gernic_builtins.Bernhard Schommer2017-09-261-8/+0
* | Added dump-mnemonics option.Bernhard Schommer2017-09-252-0/+186
* | Remove coq warnings (#28)Bernhard Schommer2017-09-225-23/+23
* | 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