aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblockgen.v
Commit message (Expand)AuthorAgeFilesLines
* Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-071-1/+1
* CleanupLéo Gourdin2020-12-191-46/+0
* Some progress in AsmblockgenproofLéo Gourdin2020-12-171-14/+15
* intermediatet commit before builtinsLéo Gourdin2020-12-161-6/+9
* Generals lemmas for asmblockgenproofLéo Gourdin2020-12-141-12/+28
* Removing the PseudoAsm IRLéo Gourdin2020-12-131-10/+29
* Some cleanup in todosLéo Gourdin2020-12-071-12/+0
* a first working draft on ldp/stp peepholeLéo Gourdin2020-12-041-16/+16
* Adding semantics for PldpLéo Gourdin2020-12-021-18/+18
* Fixing a generation bug on shrx in AsmblockgenLéo Gourdin2020-11-261-0/+6
* This commit fix the issue #226Léo Gourdin2020-11-261-50/+57
* Preparation for postpass in aarch64 and refactoringLéo Gourdin2020-11-021-20/+20
* End of Asmblock translationLéo Gourdin2020-10-291-38/+36
* Some tests and load/store instrLéo Gourdin2020-10-291-26/+145
* If, op, and some tests with a scriptLéo Gourdin2020-10-281-6/+701
* Epilogue OK and loadimmLéo Gourdin2020-10-271-58/+96
* Merge remote-tracking branch 'origin/aarch64_asmblockgen' into aarch64_blockLéo Gourdin2020-10-271-47/+52
|\
| * another start for AsmblockgenSylvain Boulmé2020-10-271-131/+52
* | A more convenient way to handle basic instLéo Gourdin2020-10-271-99/+18
|/
* [Draft] Flattened levels of binstLéo Gourdin2020-10-271-49/+180
* [Draft] Problems with coercionsLéo Gourdin2020-10-261-1078/+166
* aarch64 compiles again (but ccomp generates incorrect assembly)Sylvain Boulmé2020-10-231-6/+74
* [WIP: Coq compilation broken] Stub for AsmgenSylvain Boulmé2020-06-211-0/+1197
generated by cgit (git 2.34.1) at 2024-05-09 17:34:09 +0000