aboutsummaryrefslogtreecommitdiffstats
path: root/arm
Commit message (Expand)AuthorAgeFilesLines
* 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
* Removed no longer used function. Bug 22525Bernhard Schommer2017-11-091-25/+1
* Remove superfluous function.Bernhard Schommer2017-11-061-2/+0
* Fix register name of ais printing and moved label function up.Bernhard Schommer2017-10-251-4/+4
* 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-193-8/+16
* | Moved common buitlins to C2C gernic_builtins.Bernhard Schommer2017-09-261-9/+0
* | Added dump-mnemonics option.Bernhard Schommer2017-09-252-0/+4
* | Remove coq warnings (#28)Bernhard Schommer2017-09-224-35/+35
* | Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)Gergö Barany2017-09-186-16/+25
* | Strength reduction patterns for ARM mla instruction.Gergö Barany2017-09-152-0/+102
* | 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-221-6/+3
* | 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
* | 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
* | Integrated fixup code in estimated size.Bernhard Schommer2017-07-261-0/+3
* | Print_annot should produce a string.Bernhard Schommer2017-07-191-3/+8
|/
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-065-2/+37
* Formatted json printing.Bernhard Schommer2017-06-282-3/+3
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-038-27/+32
* RISC-V port and assorted changesXavier Leroy2017-04-282-0/+13
* 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-8/+8
* Remove unused open.Bernhard Schommer2017-02-061-1/+0
* Fallthrough no depends on the last instruction.Bernhard Schommer2016-12-151-4/+4
* Be more conservative in emiting constants.Bernhard Schommer2016-12-151-815/+827
* Use vfpv3 registers also in dwarf. Bug 20489Bernhard Schommer2016-11-291-5/+10
* Use 64 bit address in debug information.Bernhard Schommer2016-11-101-0/+2
* Update ARM port. Not tested yet.Xavier Leroy2016-10-2515-271/+388
* improve fixup code (bug 19792)Michael Schmidt2016-09-151-0/+2
* Add interference for indirect calls.Bernhard Schommer2016-09-151-1/+5
* Add missing fixup-code for ARM EABI (bug 19792)Michael Schmidt2016-09-141-2/+0
* add missing print operatorMichael Schmidt2016-09-141-0/+1
* Implement support for big endian arm targets.Bernhard Schommer2016-08-055-29/+60
* Merge branch 'master' of /common/repositories/git/tools/compcertBernhard Schommer2016-07-092-0/+36
|\
| * bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and __builtin_...Michael Schmidt2016-07-082-0/+36
* | Port to Coq 8.5pl2Xavier Leroy2016-07-084-17/+14
|/
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-221-1/+1
* 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-163/+156
* bug 18925, fix loading of symbols for thumb: :lower16: and :upper16: are rest...Michael Schmidt2016-05-131-1/+2
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-273-272/+157
* */TargetPrinter.ml: wrong comment attached to Init_float32 constantsXavier Leroy2016-04-091-1/+1
generated by cgit (git 2.34.1) at 2024-06-11 18:12:01 +0000