aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Remplacement de phys_eq par Z.eqb pour Allocframe (1 & 2) et Freeframe (1 & 2)Cyril SIX2019-03-071-10/+14
* Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-071-2/+8
|\
| * HACK for Pcompiw/Pcompil as wellCyril SIX2019-03-071-2/+8
* | forgot the .hDavid Monniaux2019-03-071-0/+4
|/
* HACK for the Pcompw/Pcompl memory problem (but performance decrease, to remov...Cyril SIX2019-03-061-1/+4
* Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...Sylvain Boulmé2019-03-063-3/+63
|\
| * Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-052-20/+218
| |\
| * \ Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-056-81/+24
| |\ \
| * \ \ Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-057-85/+187
| |\ \ \
| * \ \ \ Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-0224-1377/+2286
| |\ \ \ \
| * \ \ \ \ Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-02-221-5/+131
| |\ \ \ \ \
| * \ \ \ \ \ Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-02-212-26/+101
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-02-201-31/+41
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-02-2012-98/+701
| |\ \ \ \ \ \ \ \
| * | | | | | | | | mul8: loop-invariant code motionDavid Monniaux2019-02-193-3/+63
* | | | | | | | | | 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-053-5/+9
* | | | | | | | 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
* | | | | | Added long double = double by default on Kalray architectureCyril SIX2019-03-011-1/+1
* | | | | | Float conversion fixes + some more conversionsCyril SIX2019-02-2715-34/+123
* | | | | | 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
* | | | | | Changing the way floats are compared (script using reltol and abstol comparison)Cyril SIX2019-02-274-5/+99
* | | | | | 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-254-572/+606
* | | | | | 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
| |_|_|/ |/| | |
generated by cgit (git 2.34.1) at 2024-07-12 05:55:44 +0000