aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-0813-80/+183
|\
| * Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0411-286/+1393
| |\
| | * 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-021-2/+2
| | * [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 branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-1812-63/+109
| |\ \
| | * | Add support for __builtin_fabsfXavier Leroy2020-07-272-0/+6
| | * | Introduce additional "branch" build information.Bernhard Schommer2020-07-081-2/+2
| | * | Move shared code in new file.Bernhard Schommer2020-06-286-5/+44
| | * | Eliminate known builtins whose result is ignoredXavier Leroy2020-06-252-40/+54
| | * | Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-212-2/+2
| | * | Move reserved_registers to CPragmas.Bernhard Schommer2020-04-202-7/+1
* | | | start checking for bugsDavid Monniaux2020-12-021-2/+115
* | | | attempt at initial analysisDavid Monniaux2020-12-021-1/+35
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-024-5/+487
|\ \ \ \ | | |_|/ | |/| |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassCyril SIX2020-12-013-8/+161
| |\ \ \
| * | | | Ignore loopback edges on tail-duplicateCyril SIX2020-12-011-0/+2
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-241-2/+2
| |\ \ \ \
| * \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-194-257/+672
| |\ \ \ \ \
| * \ \ \ \ \ 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-053-28/+109
| |\ \ \ \ \ \
| * \ \ \ \ \ \ 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-034-35/+114
| |\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-313-17/+118
| |\ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ 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-294-48/+107
| |\ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-283-40/+24
| |\ \ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-274-19/+110
| |\ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | improved CSE3David Monniaux2020-10-271-12/+12
| * | | | | | | | | | | | | | progress in proofs on new CSE3David Monniaux2020-10-271-3/+34
| * | | | | | | | | | | | | | deactivate LICM by defaultDavid Monniaux2020-10-271-20/+11
| * | | | | | | | | | | | | | begin fixing CSE3 to keep more inductive stuffDavid Monniaux2020-10-272-10/+19
| * | | | | | | | | | | | | | invariant printing more aligned with RTL dumpsDavid Monniaux2020-10-271-2/+2
| * | | | | | | | | | | | | | print invariantsDavid Monniaux2020-10-271-11/+46
| * | | | | | | | | | | | | | attempt at store -> load.sDavid Monniaux2020-10-261-2/+3
| * | | | | | | | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-188-143/+845
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-021-2/+9
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepassDavid Monniaux2020-09-211-1/+482
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | | | | | risc-V now without trapping instructionsDavid Monniaux2020-09-211-0/+24
| | * | | | | | | | | | | | | | | | moved Risc-V div ValueAOp to central locationDavid Monniaux2020-09-211-0/+215
| | * | | | | | | | | | | | | | | | moved some "total" value domain functions to a central locationDavid Monniaux2020-09-211-1/+243
| * | | | | | | | | | | | | | | | | Merge branch 'kvx-work' into mppa-RTLpathSECyril SIX2020-05-2852-391/+6967
| |\| | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | [BROKEN] Merge branch 'mppa-work' into mppa-RTLpathSECyril SIX2020-04-1067-473/+5837
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | | | | | Compatibility Coq 8.11.0Cyril SIX2020-04-103-10/+10
* | | | | | | | | | | | | | | | | | | not yet the transfer functions that record predicatesDavid Monniaux2020-11-263-9/+78
* | | | | | | | | | | | | | | | | | | remains one admitDavid Monniaux2020-11-261-8/+46
generated by cgit (git 2.34.1) at 2024-06-02 17:33:16 +0000