aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-0818-115/+48
|\
| * Error when using -main without -interpXavier Leroy2020-12-061-0/+2
| * PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| * ARM modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| * AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-8/+11
| * Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-0612-99/+23
* | 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
| |\ \ \ \ \ \ \
generated by cgit (git 2.34.1) at 2024-05-19 04:46:18 +0000