aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmgen.v
Commit message (Expand)AuthorAgeFilesLines
* fix aarch64 merge?Léo Gourdin2021-03-291-0/+466
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-467/+0
|\
| * AArch64: macOS portXavier Leroy2020-12-261-2/+3
* | Adding fp stores pairLéo Gourdin2021-01-201-0/+6
* | Adding fp loads pairLéo Gourdin2021-01-201-4/+10
* | Merge remote-tracking branch 'origin/aarch64-asmblockgenproof' into aarch64-p...Léo Gourdin2020-12-201-3/+2
|\ \
| * | Removing the PseudoAsm IRLéo Gourdin2020-12-131-3/+2
* | | Big improvment in peephole, changing LDP/STP semanticsLéo Gourdin2020-12-101-8/+8
|/ /
* | a first working draft on ldp/stp peepholeLéo Gourdin2020-12-041-10/+18
* | Adding semantics for PldpLéo Gourdin2020-12-021-14/+21
* | Removing OrigAsmgen by moving the necessary functions in Asmgen.v Léo Gourdin2020-11-251-0/+77
* | Restoring asmgenproof on multiple labels issueLéo Gourdin2020-11-241-4/+4
* | Dumb (identity) scheduling working and integratedLéo Gourdin2020-11-031-2/+2
* | Author and stash single label Asmgenproof after mergeLéo Gourdin2020-11-021-0/+1
* | Merge branch 'aarch64_block_multiple_labels' into aarch64-postpassLéo Gourdin2020-11-021-4/+4
|\ \
| * | Yarpgen C file to test multiple labels and corresponding codeLéo Gourdin2020-11-011-4/+4
* | | Preparation for postpass in aarch64 and refactoringLéo Gourdin2020-11-021-6/+7
|/ /
* | Bugfix in AsmgenLéo Gourdin2020-10-291-1/+1
* | Found a bug in Asmgen about iregsp constructorLéo Gourdin2020-10-291-9/+9
* | aarch64 compiles again (but ccomp generates incorrect assembly)Sylvain Boulmé2020-10-231-5/+5
* | Adding buitin_args lemmasLéo Gourdin2020-10-211-1/+1
* | Prove exec_body_dont_move_PCJustus Fasse2020-08-181-5/+5
* | Simplify unfold_bblock and complete unfold_body's case in find_instr_bblockJustus Fasse2020-07-291-9/+2
* | backward decomposition of the proofSylvain Boulmé2020-07-221-1/+1
* | Add dynamically checked assumption to simplify AsmgenproofJustus Fasse2020-07-211-9/+23
* | "we must check that the generated code contains less than [2^32] instructions...Justus Fasse2020-07-151-2/+3
* | Generate both Pcsel and PfselJustus Fasse2020-07-131-1/+12
* | Finish proof of Lemma symbol_high_lowJustus Fasse2020-07-091-3/+3
* | Implement unfold function from Asmblock to AsmJustus Fasse2020-07-091-2/+299
* | restauring Coq compilation with STUBSSylvain Boulmé2020-06-221-2/+15
* | [WIP: Coq compilation broken] Stub for AsmgenSylvain Boulmé2020-06-211-1162/+23
* | disable leaf function removal of return address restoration due to memcpy ove...David Monniaux2020-03-271-2/+5
* | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-271-2/+4
|\ \
| * | removed RA restorationDavid Monniaux2020-03-251-2/+4
| |/
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-8/+14
|\ \
| * | 2-instruction signed division by two on Aarch64David Monniaux2020-01-151-8/+14
| |/
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-12-091-1/+6
|\|
| * Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-281-1/+6
* | Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc...David Monniaux2019-09-201-3/+8
|/
* AArch64 portXavier Leroy2019-08-081-0/+1151
generated by cgit (git 2.34.1) at 2024-05-09 03:08:15 +0000