aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asm.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-1/+1
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* | quick fixcommentsLéo Gourdin2021-02-161-1/+1
* | Adding fp stores pairLéo Gourdin2021-01-201-3/+4
* | Adding fp loads pairLéo Gourdin2021-01-201-7/+20
* | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-071-60/+6
* | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-171-2/+8
|\|
| * AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-061-4/+4
| * Added implementation for fmin/fmax for aarch64.Bernhard Schommer2020-11-061-0/+4
| * AArch64 implementation of __builtin_ctz*Xavier Leroy2020-07-271-0/+2
* | Big improvment in peephole, changing LDP/STP semanticsLéo Gourdin2020-12-101-20/+20
* | a first working draft on ldp/stp peepholeLéo Gourdin2020-12-041-18/+46
* | Adding semantics for PldpLéo Gourdin2020-12-021-3/+27
* | Proof of Pfmovimm fine tuned OK, moving float checks in AsmLéo Gourdin2020-11-261-3/+41
* | fix the semantics ?Sylvain Boulmé2020-11-181-2/+2
* | Preparation for postpass in aarch64 and refactoringLéo Gourdin2020-11-021-10/+10
* | aarch64 compiles again (but ccomp generates incorrect assembly)Sylvain Boulmé2020-10-231-9/+530
* | Prove exec_body_dont_move_PCJustus Fasse2020-08-181-4/+4
* | Add dynamically checked assumption to simplify AsmgenproofJustus Fasse2020-07-211-1/+1
* | aarch64/Asm: Fix `Error: Pattern "PC" is redundant in this clause.`Justus Fasse2020-07-061-1/+1
* | [WIP: Coq compilation broken] Stub for AsmgenSylvain Boulmé2020-06-211-498/+32
|/
* Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-031-1/+3
* Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-211-3/+1
* AArch64 portXavier Leroy2019-08-081-0/+1312
generated by cgit (git 2.34.1) at 2024-05-09 09:56:14 +0000