aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
* fix aarch64 merge?Léo Gourdin2021-03-291-0/+1836
* [WIP: Coq compilation broken] Stub for AsmgenSylvain Boulmé2020-06-211-2138/+0
* disable leaf function removal of return address restoration due to memcpy ove...David Monniaux2020-03-271-3/+6
* Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-271-2/+28
|\
| * better epilogue proofDavid Monniaux2020-03-251-8/+18
| * removed RA restorationDavid Monniaux2020-03-251-1/+17
* | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-261-187/+436
|\|
| * RA is preservedDavid Monniaux2020-03-251-12/+20
| * Asmgenproof1David Monniaux2020-03-241-1/+3
| * transl_addressing_correctDavid Monniaux2020-03-241-4/+9
| * transl_op_correctDavid Monniaux2020-03-241-10/+14
| * transl_condDavid Monniaux2020-03-241-143/+332
| * progress in proofs about RADavid Monniaux2020-03-241-16/+57
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-14/+38
|\ \
| * | 2-instruction signed division by two on Aarch64David Monniaux2020-01-151-14/+38
| |/
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-12-091-1/+1
|\|
| * Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-281-1/+1
* | Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc...David Monniaux2019-09-201-1/+1
|/
* Asmgenproof1: useless unfolding in proof scripts causing "omega" to failXavier Leroy2019-09-111-3/+3
* AArch64 portXavier Leroy2019-08-081-0/+1836
generated by cgit (git 2.34.1) at 2024-05-09 18:14:37 +0000