aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/PostpassSchedulingproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactorCyril SIX2019-04-081-5/+5
|\
| * relecture sylvainSylvain Boulmé2019-04-051-5/+5
* | #91 Removed completely the duplicated semantics in AsmblockCyril SIX2019-04-051-20/+16
|/
* #90 Asmvliw/Asmblock refactoring attemptCyril SIX2019-04-051-2/+2
* Merge remote-tracking branch 'origin/mppa_k1c' into mppa-workCyril SIX2019-04-031-17/+5
|\
| * cleaning Asmvliw semanticsSylvain Boulmé2019-04-011-17/+5
* | Preuve des load/store registre registre. Reste des modifs mineures dans les p...Cyril SIX2019-04-031-5/+4
* | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yetCyril SIX2019-04-021-18/+46
|/
* Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptableCyril SIX2019-03-291-3/+173
|\
| * Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-281-3/+173
| |\
| | * slight simplificationSylvain Boulmé2019-03-231-5/+4
| | * fix for Coq.8.8 ??Sylvain Boulmé2019-03-221-2/+0
| | * Décomposition de la preuve en une forward_simu_par_stuck et une forward_simu...Cyril SIX2019-03-221-1/+4
| | * simplification of the proofSylvain Boulmé2019-03-211-26/+66
| | * yet another step backwardSylvain Boulmé2019-03-201-18/+39
| | * one step further...Sylvain Boulmé2019-03-201-6/+28
| | * premier decoupageSylvain Boulmé2019-03-201-2/+56
| | * Integrating Asmvliw.v in the proof chainCyril SIX2019-03-201-10/+24
| | * Idée de preuve VLIWCyril SIX2019-03-181-2/+21
| | * definition of VLIW semanticsSylvain Boulmé2019-03-141-5/+4
* | | on avance sur la jumptableDavid Monniaux2019-03-221-0/+1
|/ /
* / 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 remaining...Cyril SIX2019-03-051-12/+0
* 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
* 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
generated by cgit (git 2.34.1) at 2024-07-06 17:27:47 +0000