aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmgen.v
Commit message (Expand)AuthorAgeFilesLines
* 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