aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Prove find_instr_bblock_tailJustus Fasse2020-07-301-2/+89
* Simplify unfold_bblock and complete unfold_body's case in find_instr_bblockJustus Fasse2020-07-291-3/+74
* Find label in base case of find_instr_bblockJustus Fasse2020-07-281-2/+18
* Messy progress on builtin-case of exec_exit_simulation_plusJustus Fasse2020-07-281-10/+25
* Messy progress on exec_exit_simulation_plusJustus Fasse2020-07-281-3/+27
* Rename/repurpose cf_instruction_simulated for exec_cfi_simulationJustus Fasse2020-07-281-179/+150
* Begin proof of exec_exit_simulation_plusJustus Fasse2020-07-271-0/+42
* Playing around with find_instr_bblock's base caseJustus Fasse2020-07-271-7/+25
* Replace some auto-generated namesJustus Fasse2020-07-271-3/+3
* Move position of n in formulation of find_instr_bblockJustus Fasse2020-07-271-4/+4
* Idea for find_instr_bblock's recursive caseJustus Fasse2020-07-271-7/+35
* Factorize common proof-pattern as lemmasJustus Fasse2020-07-271-8/+30
* Simplify premisesJustus Fasse2020-07-241-12/+9
* Remove unnecessary premiseJustus Fasse2020-07-241-4/+3
* Remove trailing whitespaceJustus Fasse2020-07-241-4/+4
* Complete size_headerJustus Fasse2020-07-241-1/+66
* Complete bblock_size_auxJustus Fasse2020-07-241-1/+24
* Complete bblock_size_aux_posJustus Fasse2020-07-241-1/+6
* proof of exec_header_simulationSylvain Boulmé2020-07-231-10/+91
* Complete bblock_non_emptyJustus Fasse2020-07-231-1/+10
* Remove trailing whitespaceJustus Fasse2020-07-221-6/+6
* Complete proof of exec_exit_simulation_starJustus Fasse2020-07-221-2/+10
* backward decomposition of the proofSylvain Boulmé2020-07-221-20/+165
* suggestion of simpler nameSylvain Boulmé2020-07-171-1/+1
* suggestion of translation from find_bblock to find_instrSylvain Boulmé2020-07-171-0/+22
* Less auto-generated namesJustus Fasse2020-07-151-36/+36
* 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
|/
generated by cgit (git 2.34.1) at 2024-07-14 07:54:28 +0000