aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
...
* 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 ↵Cyril SIX2019-03-052-74/+10
| | | | extraction
* 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 ↵Cyril SIX2019-03-053-46/+66
| | | | remaining in Asmblockdeps)
* 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
|
* Complete proof of forward_simu_control in AsmblockdepsCyril SIX2019-02-221-1/+109
|
* Separated forward_simulation into body and exit (Asmblockdeps)Cyril SIX2019-02-211-5/+23
|
* Starting forward simulation Asmblock -> AsmblockdepsCyril SIX2019-02-211-22/+97
|
* PostpassScheduling: outcome' = option state'Cyril SIX2019-02-211-4/+4
|
* Finished the compilation of Asmblock to AbstractbbCyril SIX2019-02-201-31/+41
|
* Added compilation in abstractbb of most of the basic instructionsCyril SIX2019-02-201-6/+76
|
* Added compilation of control instructions to AbstractBBCyril SIX2019-02-201-3/+74
|
* Remove unnecessary and error prone FR constructor for pregsCyril SIX2019-02-204-11/+5
|
* Added useful operators for the control flow instructionsCyril SIX2019-02-201-3/+74
|
* Problème résolu en prenant les noms de resources comme étant des PosCyril SIX2019-02-201-4/+14
|
* Stuck at module IDTCyril SIX2019-02-201-1/+10
|
* Finished specialization of the Abstractbb languageCyril SIX2019-02-201-89/+253
|
* WIP sur Asmblockdeps.vCyril SIX2019-02-201-0/+168
|
* [BROKEN] trying to generalize Sylvain's abstract bb to include a genv.Cyril SIX2019-02-207-87/+133
| | | | FIXME - DepExampleDemo.v
* use a Pfsd (store double) and not a Pfss (store single) for storing doublesDavid Monniaux2019-02-181-1/+1
|
* reversed the register allocation ordering between float and int registers, ↵David Monniaux2019-02-181-2/+2
| | | | to avoid contention
* Rajout d'opérateurs flottants, travail sur les tests --> à continuerCyril SIX2019-02-155-114/+169
|
* FIX axiom to be realized issueCyril SIX2019-02-152-2/+35
|
* Generalizing state' in PostpassSchedulingCyril SIX2019-02-141-32/+23
|
* More lemmas in PostpassSchedulingCyril SIX2019-02-141-6/+26
|
* Some more lemma proving in PostpassSchedulingCyril SIX2019-02-141-10/+73
|
generated by cgit (git 2.34.1) at 2024-07-12 07:40:55 +0000