aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
|\|
| * Fixing issue with loops having branches leading to goto backedgeCyril SIX2020-11-052-27/+32
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-055-31/+114
|\|
| * Fixing get_loop_headers + alternative get_inner_loops (commented, not active)Cyril SIX2020-11-042-27/+107
| * Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2020-11-041-1/+2
| |\
| | * youtube linkSylvain Boulmé2020-11-041-1/+2
| | * Revert "Embed the short video with subtitles..."Sylvain Boulmé2020-11-041-10/+2
| | * Embed the short video with subtitles...Sylvain Boulmé2020-11-041-2/+10
| * | move loop rotate downDavid Monniaux2020-11-041-4/+5
| * | do not print "refining" unless askedDavid Monniaux2020-11-041-1/+2
| |/
* | 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
|\|
| * do not print "updates" to nodesDavid Monniaux2020-11-041-1/+2
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-037-36/+121
|\|
| * refixcse3David Monniaux2020-11-032-34/+53
| * Loop Rotate with -flooprotateCyril SIX2020-11-035-1/+67
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-315-17/+121
|\|
generated by cgit (git 2.34.1) at 2024-07-04 00:13:36 +0000