aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* volatile storesDavid Monniaux2019-03-101-43/+40
* volatile loadDavid Monniaux2019-03-101-37/+37
* Added error message for Odivfs in AsmblockgenCyril SIX2019-03-081-0/+1
* Rajout de commentaires sur les instructions non émisesCyril SIX2019-03-081-8/+8
* Fix for the compw immediate problemCyril SIX2019-03-081-7/+17
* Minor fix on TargetPrinter (coqint instead of coqint64 for adequate types)Cyril SIX2019-03-081-8/+8
* Refactorisation des load et des storeCyril SIX2019-03-083-62/+40
* Reverting the hack introduces on Pcompw etc..Cyril SIX2019-03-081-14/+3
* Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patchCyril SIX2019-03-085-42/+387
|\
| * Preuves du branchement avec des floatCyril SIX2019-03-071-25/+242
| * Fix minor proofCyril SIX2019-03-073-27/+142
| * Remplacement de phys_eq par Z.eqb pour Allocframe (1 & 2) et Freeframe (1 & 2)Cyril SIX2019-03-071-10/+14
| * HACK for Pcompiw/Pcompil as wellCyril SIX2019-03-071-2/+8
| * HACK for the Pcompw/Pcompl memory problem (but performance decrease, to remov...Cyril SIX2019-03-061-1/+4
* | Fixing Asmblockdeps proofsCyril SIX2019-03-081-147/+21
* | Refactorized Asmblock exec_basic_instrCyril SIX2019-03-082-105/+121
* | axioms on pointer comparison removed !Sylvain Boulmé2019-03-071-11/+12
* | remove dep of exec_arith_instr on memory.Sylvain Boulmé2019-03-073-66/+77
* | Experiment Patch of Memory ModelSylvain Boulmé2019-03-073-21/+48
|/
* fix eq sur OIncremPCSylvain Boulmé2019-03-061-7/+14
* quick fix of equalities issuesSylvain Boulmé2019-03-052-1/+10
* Added pretty printersCyril SIX2019-03-051-19/+208
* fix extraction of ImpConfigSylvain Boulmé2019-03-051-2/+5
* compilation of ImpIOOraclesSylvain Boulmé2019-03-052-4/+8
* No more axioms remaining (scheduling completely proven), however error at ext...Cyril SIX2019-03-052-74/+10
* C'est moi qui avait fait des betises avec CoqIDE, ça remarcheCyril SIX2019-03-051-8/+26
* [BROKEN] error with the new is_constant and is_constant_correctCyril SIX2019-03-051-26/+8
* forward_simu_alt proof AsmblockdepsCyril SIX2019-03-051-1/+6
* remove cumbersome dependency on genv in bblock_eq_testSylvain Boulmé2019-03-054-33/+55
* No more axiom remaining in PostpassScheduling.v (but still a couple remaining...Cyril SIX2019-03-053-46/+66
* bblock_equiv_reduce Asmblockdeps.vCyril SIX2019-03-041-4/+42
* (Unsafe) coercion of ??bool into boolSylvain Boulmé2019-03-022-2/+19
* Added double comparisonsCyril SIX2019-03-018-23/+118
* Ajouté la négation des comparateurs singleCyril SIX2019-03-013-3/+42
* Implemented float comparisons (no branching yet, and no negation)Cyril SIX2019-03-018-29/+132
* Ointuofsingle doneCyril SIX2019-03-016-32/+23
* Float conversion fixes + some more conversionsCyril SIX2019-02-2710-27/+114
* Fixed some additional operands inversionsCyril SIX2019-02-271-4/+4
* FIX the order of operands of float sub was invertedCyril SIX2019-02-271-2/+2
* Removing unused cases AsmblockgenCyril SIX2019-02-271-3/+0
* Proving the trans_block_header axiomsCyril SIX2019-02-274-713/+719
* Proving a few more lemmas AsmblockdepsCyril SIX2019-02-271-15/+38
* Proved forward_simu_stuck in Asmblockdeps.vCyril SIX2019-02-261-15/+132
* Finished trans_block_reverse_stuckCyril SIX2019-02-261-6/+26
* Proving two lemmas of trans_block_reverse_stuck AsmblockdepsCyril SIX2019-02-251-5/+46
* Splitting trans_block_reverse_stuck into smaller lemmasCyril SIX2019-02-251-8/+73
* Plugged Asmblockdeps into PostpassSchedulingCyril SIX2019-02-253-572/+605
* Finished the forward_simu of Asmblockdeps.vCyril SIX2019-02-251-6/+90
* forward_simu_basic prouvé --> à prouver, trans_arith_correct (Asmblockdeps)Cyril SIX2019-02-221-2/+28
* forward_simu_basic proof until Pallocframe in Asmblockdeps.vCyril SIX2019-02-221-9/+94
generated by cgit (git 2.34.1) at 2024-07-04 00:57:07 +0000