aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Fixing test/regression for KVXv3.8_kvxCyril SIX2020-12-076-2/+409
* Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-04104-1053/+11993
|\
| * CommentCyril SIX2020-12-041-0/+1
| * Less aggressive tail duplicationCyril SIX2020-12-041-6/+11
| * Clean-up debugCyril SIX2020-12-041-4/+2
| * Fixed infinite loop on find_last_node_before_loopCyril SIX2020-12-041-3/+6
| * Slight perf improvementCyril SIX2020-12-022-4/+4
| * [expensive] Behavior change when the loop has two final instructionsCyril SIX2020-12-021-9/+57
| * Duplicateaux: Generalization of look_aheadCyril SIX2020-12-011-3/+5
| * Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassCyril SIX2020-12-016-11/+161
| |\
| | * store2_soundDavid Monniaux2020-11-251-1/+1
| | * clever_kill_store_soundDavid Monniaux2020-11-251-7/+5
| | * kill_store_soundDavid Monniaux2020-11-251-0/+49
| | * two lemmas admittedDavid Monniaux2020-11-253-9/+115
| | * missing lemmasDavid Monniaux2020-11-251-0/+21
| | * pointer_eq copiedDavid Monniaux2020-11-256-0/+86
| * | Ignore loopback edges on tail-duplicateCyril SIX2020-12-011-0/+2
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-2413-31/+343
| |\|
| | * tiny simplification in Tunnelingaux.mlSylvain Boulmé2020-11-241-2/+2
| | * bug #223 fix on PPCDavid Monniaux2020-11-232-3/+73
| | * bug #223 fix for ARMDavid Monniaux2020-11-232-3/+76
| | * bug #223 fix on x86 / x86-64David Monniaux2020-11-232-4/+80
| | * fix wrong version of file on AArch64David Monniaux2020-11-231-1/+4
| | * Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2020-11-232-3/+14
| | |\
| | | * fix bug #223 on Risc-VDavid Monniaux2020-11-232-3/+14
| | * | fix bug #223 on AArch64David Monniaux2020-11-231-3/+72
| | |/
| | * correction bug #223 sur KVXDavid Monniaux2020-11-232-12/+22
| * | prepass scheduling proof finished !Sylvain Boulmé2020-11-201-24/+56
| * | merge nouveau tunnelingDavid Monniaux2020-11-191-1/+1
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-198-270/+728
| |\|
| | * for 2010-11-18 Kalray releaseDavid Monniaux2020-11-191-1/+1
| | * minor fix in coq2html commentSylvain Boulmé2020-11-161-1/+2
| | * Tunneling: improved elimination of conditionsSylvain Boulmé2020-11-166-259/+673
| | * Proof of UnionFind.pathlen_unionSylvain Boulmé2020-11-161-10/+53
| * | seval_builtin_sval_preservedDavid Monniaux2020-11-171-1/+4
| * | a little lemma on list of builtinsDavid Monniaux2020-11-171-2/+15
| * | there remains two tricky casesDavid Monniaux2020-11-161-3/+14
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-062-27/+32
| |\|
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-055-31/+114
| |\ \
| * | | disable debug printing in schedulerDavid Monniaux2020-11-042-7/+9
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-041-1/+2
| |\ \ \
| * \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-037-36/+121
| |\ \ \ \
| * \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-315-17/+121
| |\ \ \ \ \
| * \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-304-168/+78
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-295-48/+109
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-284-42/+27
| |\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-277-63/+166
| |\ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-277-10/+277
| |\ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | improved CSE3David Monniaux2020-10-271-12/+12
| * | | | | | | | | | | progress in proofs on new CSE3David Monniaux2020-10-271-3/+34