aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Expand)AuthorAgeFilesLines
* aarch64 compiles again (but ccomp generates incorrect assembly)Sylvain Boulmé2020-10-239-612/+961
* [Draft] Improvements on buitin cfi proof and new lemmas for set_res.Léo Gourdin2020-10-221-1/+143
* Adding buitin_args lemmasLéo Gourdin2020-10-213-24/+68
* update commentsLéo Gourdin2020-10-201-17/+14
* cfi_simu finishedLéo Gourdin2020-10-201-15/+36
* exec_body_simulation_plus_gen proof OKLéo Gourdin2020-10-201-11/+35
* New lemmas and subcases for cfi_simuLéo Gourdin2020-10-191-49/+68
* Some subcases for exec cfi simuLéo Gourdin2020-10-191-95/+68
* Typo in label_pos_preserved hypLéo Gourdin2020-10-191-2/+1
* Improvements in AsmgenproofLéo Gourdin2020-10-191-32/+111
* Merge remote-tracking branch 'origin/aarch64_block_bodystar' into aarch64_blo...Léo Gourdin2020-10-161-222/+114
|\
| * replace exec_body_simulation_star' by exec_body_simulation_plus_genSylvain Boulmé2020-10-161-222/+114
* | Pb, Pbc, and nextinst incrPC preserved lemmaLéo Gourdin2020-10-161-41/+79
|/
* label and goto_label preserved lemmasLéo Gourdin2020-10-161-3/+51
* exec_basic_simulation proof OKLéo Gourdin2020-10-161-32/+23
* PArithComp subcases OKLéo Gourdin2020-10-161-110/+75
* Progress in exec_basic_simuLéo Gourdin2020-10-151-104/+148
* Some subcases for exec_basic_simuLéo Gourdin2020-10-141-86/+49
* an idea to tackle PArithComparisonPPSylvain Boulmé2020-10-141-2/+43
* draft commit for the Pallocframe proof subcaseLéo Gourdin2020-10-141-2/+15
* Pstore preserved lemmaLéo Gourdin2020-10-141-3/+64
* Other subcases for PArith are done.Léo Gourdin2020-10-141-8/+29
* Draft commit on the PArithComparisonPP ProofLéo Gourdin2020-10-141-14/+72
* Simplifying Ltac and fixing a bug in AsmBlock semanticsLéo Gourdin2020-10-132-11/+31
* Fixing the propagation of the new BOUNDED hypLéo Gourdin2020-10-131-8/+20
* Proof for PmovzLéo Gourdin2020-10-131-7/+29
* Adding a lemma next_instr_preservedLéo Gourdin2020-10-121-7/+56
* Continue the proof of exec_basic_simulationLéo Gourdin2020-10-111-18/+12
* Adding a lemma for exec load propagation.Léo Gourdin2020-10-111-25/+27
* Merge branch 'aarch64_block_bodystar' of gricad-gitlab.univ-grenoble-alpes.fr...Léo Gourdin2020-10-101-10/+14
|\
| * Merge branch 'aarch64_block_bodystar' of gricad-gitlab.univ-grenoble-alpes.fr...Sylvain Boulmé2020-10-101-0/+14
| |\
| * | Still generalizing exec_body_simulation_plus for an inductive proofSylvain Boulmé2020-10-091-10/+14
* | | More general version of load preservation lemma.Léo Gourdin2020-10-101-7/+25
| |/ |/|
* | Adding a lemma for load preservationLéo Gourdin2020-10-101-0/+14
|/
* slight refactoring, in order to avoid a duplication of the proof.Sylvain Boulmé2020-10-091-40/+36
* exec_body_simulation without star'Léo Gourdin2020-10-091-0/+101
* Replace common pattern with simpler lemma.Justus Fasse2020-09-211-29/+16
* Proof of exec_body_simulation_plusJustus Fasse2020-09-211-1/+238
* Move a couple of lemmas up in the fileJustus Fasse2020-09-211-68/+68
* Admitted lemma for exec_basic_simulation.Justus Fasse2020-09-211-0/+9
* Prove exec_body_dont_move_PCJustus Fasse2020-08-184-42/+112
* Proof for size_of_blocks_max_posJustus Fasse2020-08-051-18/+50
* Minor cleanup of find_instr_bblockJustus Fasse2020-07-301-11/+10
* Complete proof of find_instr_bblockJustus Fasse2020-07-301-3/+30
* Absurd case in find_instr_bblockJustus Fasse2020-07-301-1/+107
* 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-292-12/+76
* 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
generated by cgit (git 2.34.1) at 2024-06-03 00:22:09 +0000