aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
...
* | | First go at showing that translated cfi behave the sameJustus Fasse2020-07-151-0/+191
* | | Add lemma showing 1 <= Ptrofs.max_unsignedJustus Fasse2020-07-151-2/+8
* | | Miscellaneous lemmas that I used at some point while experimentingJustus Fasse2020-07-151-0/+84
* | | Add definition of match_internalJustus Fasse2020-07-151-0/+18
* | | Revert back to original definition of match_statesJustus Fasse2020-07-121-172/+8
* | | Change definition of match_statesJustus Fasse2020-07-101-8/+172
* | | Start AsmgenproofJustus Fasse2020-07-091-3/+69
* | | Finish proof of Lemma symbol_high_lowJustus Fasse2020-07-091-3/+8
* | | fix linker model in AsmblockSylvain Boulmé2020-06-221-2/+13
* | | restauring Coq compilation with STUBSSylvain Boulmé2020-06-221-0/+127
* | | [WIP: Coq compilation broken] Stub for AsmgenSylvain Boulmé2020-06-211-1101/+0
|/ /
* | disable leaf function removal of return address restoration due to memcpy ove...David Monniaux2020-03-271-2/+2
* | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-271-1/+6
|\ \
| * | removed RA restorationDavid Monniaux2020-03-251-1/+6
* | | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-261-38/+96
|\| |
| * | RA is preservedDavid Monniaux2020-03-251-6/+16
| * | proof forwardDavid Monniaux2020-03-251-1/+4
| * | proof forwardDavid Monniaux2020-03-251-5/+15
| * | proof forwardDavid Monniaux2020-03-251-6/+24
| * | progress in proofs about RADavid Monniaux2020-03-241-20/+35
| * | exec_straight_stepsDavid Monniaux2020-03-241-5/+7
| |/
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-2/+2
|\ \
| * | 2-instruction signed division by two on Aarch64David Monniaux2020-01-151-2/+2
| |/
* / Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc...David Monniaux2019-09-201-3/+15
|/
* AArch64 portXavier Leroy2019-08-081-0/+1026
generated by cgit (git 2.34.1) at 2024-07-12 05:14:02 +0000