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