Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Fixing test/regression for KVXv3.8_kvx | Cyril SIX | 2020-12-07 | 6 | -2/+409 |
* | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 104 | -1053/+11993 |
|\ | |||||
| * | Comment | Cyril SIX | 2020-12-04 | 1 | -0/+1 |
| * | Less aggressive tail duplication | Cyril SIX | 2020-12-04 | 1 | -6/+11 |
| * | Clean-up debug | Cyril SIX | 2020-12-04 | 1 | -4/+2 |
| * | Fixed infinite loop on find_last_node_before_loop | Cyril SIX | 2020-12-04 | 1 | -3/+6 |
| * | Slight perf improvement | Cyril SIX | 2020-12-02 | 2 | -4/+4 |
| * | [expensive] Behavior change when the loop has two final instructions | Cyril SIX | 2020-12-02 | 1 | -9/+57 |
| * | Duplicateaux: Generalization of look_ahead | Cyril SIX | 2020-12-01 | 1 | -3/+5 |
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | Cyril SIX | 2020-12-01 | 6 | -11/+161 |
| |\ | |||||
| | * | store2_sound | David Monniaux | 2020-11-25 | 1 | -1/+1 |
| | * | clever_kill_store_sound | David Monniaux | 2020-11-25 | 1 | -7/+5 |
| | * | kill_store_sound | David Monniaux | 2020-11-25 | 1 | -0/+49 |
| | * | two lemmas admitted | David Monniaux | 2020-11-25 | 3 | -9/+115 |
| | * | missing lemmas | David Monniaux | 2020-11-25 | 1 | -0/+21 |
| | * | pointer_eq copied | David Monniaux | 2020-11-25 | 6 | -0/+86 |
| * | | Ignore loopback edges on tail-duplicate | Cyril SIX | 2020-12-01 | 1 | -0/+2 |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-24 | 13 | -31/+343 |
| |\| | |||||
| | * | tiny simplification in Tunnelingaux.ml | Sylvain Boulmé | 2020-11-24 | 1 | -2/+2 |
| | * | bug #223 fix on PPC | David Monniaux | 2020-11-23 | 2 | -3/+73 |
| | * | bug #223 fix for ARM | David Monniaux | 2020-11-23 | 2 | -3/+76 |
| | * | bug #223 fix on x86 / x86-64 | David Monniaux | 2020-11-23 | 2 | -4/+80 |
| | * | fix wrong version of file on AArch64 | David Monniaux | 2020-11-23 | 1 | -1/+4 |
| | * | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2020-11-23 | 2 | -3/+14 |
| | |\ | |||||
| | | * | fix bug #223 on Risc-V | David Monniaux | 2020-11-23 | 2 | -3/+14 |
| | * | | fix bug #223 on AArch64 | David Monniaux | 2020-11-23 | 1 | -3/+72 |
| | |/ | |||||
| | * | correction bug #223 sur KVX | David Monniaux | 2020-11-23 | 2 | -12/+22 |
| * | | prepass scheduling proof finished ! | Sylvain Boulmé | 2020-11-20 | 1 | -24/+56 |
| * | | merge nouveau tunneling | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-19 | 8 | -270/+728 |
| |\| | |||||
| | * | for 2010-11-18 Kalray release | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| | * | minor fix in coq2html comment | Sylvain Boulmé | 2020-11-16 | 1 | -1/+2 |
| | * | Tunneling: improved elimination of conditions | Sylvain Boulmé | 2020-11-16 | 6 | -259/+673 |
| | * | Proof of UnionFind.pathlen_union | Sylvain Boulmé | 2020-11-16 | 1 | -10/+53 |
| * | | seval_builtin_sval_preserved | David Monniaux | 2020-11-17 | 1 | -1/+4 |
| * | | a little lemma on list of builtins | David Monniaux | 2020-11-17 | 1 | -2/+15 |
| * | | there remains two tricky cases | David Monniaux | 2020-11-16 | 1 | -3/+14 |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-06 | 2 | -27/+32 |
| |\| | |||||
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-05 | 5 | -31/+114 |
| |\ \ | |||||
| * | | | disable debug printing in scheduler | David Monniaux | 2020-11-04 | 2 | -7/+9 |
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-04 | 1 | -1/+2 |
| |\ \ \ | |||||
| * \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-03 | 7 | -36/+121 |
| |\ \ \ \ | |||||
| * \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-31 | 5 | -17/+121 |
| |\ \ \ \ \ | |||||
| * \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-30 | 4 | -168/+78 |
| |\ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-29 | 5 | -48/+109 |
| |\ \ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-28 | 4 | -42/+27 |
| |\ \ \ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 7 | -63/+166 |
| |\ \ \ \ \ \ \ \ \ | |||||
| * \ \ \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 7 | -10/+277 |
| |\ \ \ \ \ \ \ \ \ \ | |||||
| * | | | | | | | | | | | improved CSE3 | David Monniaux | 2020-10-27 | 1 | -12/+12 |
| * | | | | | | | | | | | progress in proofs on new CSE3 | David Monniaux | 2020-10-27 | 1 | -3/+34 |