aboutsummaryrefslogtreecommitdiffstats
path: root/arm
Commit message (Expand)AuthorAgeFilesLines
* Changed cc_varargs to an option typeBernhard Schommer2020-12-251-2/+2
* ARM modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+1
* Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-1/+1
* Move declarations of __builtin_clz* and __builtin_ctz* to C2C.mlXavier Leroy2020-07-271-13/+0
* No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-2/+0
* Added missing hint database name.Bernhard Schommer2020-06-301-1/+1
* Move shared code in new file.Bernhard Schommer2020-06-282-18/+0
* Remove the `can_reserve_register` function.Bernhard Schommer2020-06-282-5/+0
* Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
* Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-206/+0
* Support re-normalization of values returned by function callsXavier Leroy2020-02-211-0/+6
* Refine the type of function results in AST.signatureXavier Leroy2020-02-212-15/+13
* Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-034-1/+8
* Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-214-8/+1
* Reworked json export.Bernhard Schommer2019-09-121-18/+22
* Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-111-2/+2
|\
| * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
* | Compatibility for OCaml 4.08.1Bernhard Schommer2019-09-051-1/+1
* | bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-0/+5
|/
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-15/+55
* Remove the cparser/Builtins moduleXavier Leroy2019-07-171-2/+2
* Add floating-point square root and fused multiply-addXavier Leroy2019-07-171-0/+5
* 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
generated by cgit (git 2.34.1) at 2024-06-02 22:05:07 +0000