aboutsummaryrefslogtreecommitdiffstats
path: root/arm
Commit message (Expand)AuthorAgeFilesLines
* Revised specification of NaN payload behaviorXavier Leroy2019-07-121-17/+39
* Extended asm: print register names according to their typesXavier Leroy2019-06-171-3/+3
* Perform constant propagation and strength reduction on conditional movesXavier Leroy2019-06-172-2/+36
* Added Pfmovite to list of known mnemonic names.Bernhard Schommer2019-06-061-1/+1
* ARM: select is not supported at type TlongXavier Leroy2019-06-062-2/+11
* ARM: Fix expansion of FP conditional moveXavier Leroy2019-05-261-2/+2
* Implement a `Osel` operation for ARMXavier Leroy2019-05-2012-7/+115
* Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-2/+2
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-1/+2
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-1/+1
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-14/+15
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-124-6/+10
* Import prim token notations before using them, continuedXavier Leroy2018-08-271-0/+1
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-012-3/+12
* Print symbols as symbols.Bernhard Schommer2018-03-081-16/+16
* Fix register naming for stack pointer.Bernhard Schommer2018-03-081-1/+1
* Also use binary output for arm. Fix 23172Bernhard Schommer2018-03-071-1/+1
* Fix arm compile broken by merge problems.Bernhard Schommer2018-03-061-4/+2
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-061-5/+6
* Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)Xavier Leroy2018-02-162-15/+49
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-1/+1
* Remove mnemonics not exported to JSON from mnemonics listMichael Schmidt2018-01-091-4/+4
* 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
* Reintroduce informative comments for Pflid_lbl/Pflis_lbl in target printerMichael Schmidt2017-12-151-3/+6
* Reintroduce informative comment for Ploadsymbol_lbl in target printerMichael Schmidt2017-12-151-2/+2
* Introduce 'cmn' instruction and optimize compare-with-immediate when negated ...Michael Schmidt2017-12-156-1/+27
* Moved constant expansion into Asmexpand. (#40)Bernhard Schommer2017-12-145-318/+419
* Use instructions with immediate operands that don't need replacement by the a...Michael Schmidt2017-12-141-4/+3
* Export configured architecture to JSON (#38)Michael Schmidt2017-12-131-3/+3
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-052-10/+24
* Remove unused float_abi_type.Bernhard Schommer2017-11-291-12/+0
* 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