aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/PostpassSchedulingproof.v
Commit message (Collapse)AuthorAgeFilesLines
* The parent frame pointer is now R17 instead of R14Cyril SIX2019-03-181-3/+3
|
* Refactorisation des load et des storeCyril SIX2019-03-081-3/+3
|
* Refactorized Asmblock exec_basic_instrCyril SIX2019-03-081-1/+1
|
* No more axiom remaining in PostpassScheduling.v (but still a couple ↵Cyril SIX2019-03-051-12/+0
| | | | remaining in Asmblockdeps)
* Proving the trans_block_header axiomsCyril SIX2019-02-271-672/+672
|
* Proving verify_schedule_correct with axiomsCyril SIX2019-02-141-14/+0
|
* Added Ointofsingle + floatconv unit testCyril SIX2019-02-121-1/+1
|
* Added OsingleofintCyril SIX2019-02-121-2/+5
|
* Minor refactorizationCyril SIX2019-02-121-12/+0
|
* Proof of axiom verified_schedule_headerCyril SIX2019-02-121-59/+0
|
* Proving the axiom verified_schedule_single_instCyril SIX2019-02-121-2/+0
|
* Proving verified_schedule_size axiomCyril SIX2019-02-111-5/+0
|
* Un peu de refactorisationCyril SIX2019-02-071-60/+2
|
* Removing the low_half axiomCyril SIX2019-02-051-8/+3
|
* Preuves (en dehors du verified_schedule) terminées dans PostpassSchedulingproofCyril SIX2019-02-041-6/+44
|
* Proof of transf_exec_control \o/Cyril SIX2019-02-041-2/+5
|
* Proof of label_pos related things in PostpassSchedulingproofCyril SIX2019-02-041-15/+104
|
* Encore de la tuyauterieCyril SIX2019-02-011-1/+91
|
* Proof of transf_blocks_verifiedCyril SIX2019-02-011-9/+46
|
* Décomposition de transf_find_bblock en lemmesCyril SIX2019-01-311-1/+22
|
* Adding a "check_size" in concat2Cyril SIX2019-01-311-13/+30
|
* Hypothèses de pc_set_add permettant de prouver le lemmeCyril SIX2019-01-291-19/+26
|
* Avancement sur exec_basic_instr_pcvar + exec_load et exec_store prennent des ↵Cyril SIX2019-01-291-33/+132
| | | | ireg au lieu de preg
* Avancement PostpassSchedulingproofCyril SIX2019-01-251-5/+69
|
* Progrès dans PostpassSchedulingproofCyril SIX2019-01-251-6/+46
|
* Un peu d'avancement sur PostpassSchedulingproofCyril SIX2019-01-241-9/+27
|
* Cleaning dans PostpassSchedulingproofCyril SIX2019-01-231-43/+20
|
* 3ème cas de transf_step_correct de PostpassSchedulingproof finiCyril SIX2019-01-231-5/+6
|
* Proof of builtin case for transf_step_correct in PostpassSchedulingproofCyril SIX2019-01-231-1/+25
|
* Adding a predicate that a builtin must be alone in its basicblockCyril SIX2019-01-231-7/+23
|
* Changement de modèle de preuve pour le 1er cas du tranf_step_correct de ↵Cyril SIX2019-01-231-14/+47
| | | | PostpassSchedulingproof
* Léger avancement PostpassSchedulingproof.vCyril SIX2019-01-221-1/+7
|
* Un poil d'avancement sur PostpassSchedulingproof.v. Corrections à faire sur ↵Cyril SIX2019-01-211-1/+47
| | | | le modèle
* Generalizing PostpassScheduling to include bblock splittingCyril SIX2018-12-051-25/+72
|
* Renaming PostpassSchedulingProof -> PostpassSchedulingproofCyril SIX2018-12-051-0/+163
generated by cgit (git 2.34.1) at 2024-07-11 22:22:17 +0000