aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* [BROKEN] Replacing the boolean -fduplicate option by an integerCyril SIX2020-03-091-4/+6
* Linearizeaux: forgotten printCyril SIX2020-03-091-1/+1
* Duplicate: getting rid of the annoying exception-based codeCyril SIX2020-03-091-46/+29
* Removing prints in Duplicateaux.mlCyril SIX2020-03-091-65/+20
* Merge remote-tracking branch 'origin/mppa-work' into mppa-work-untestedCyril SIX2020-03-0921-180/+315
|\
| * removing some coqc 8.10 warningsSylvain Boulmé2020-03-091-1/+1
| * fixed CSE2 for mppa_k1cDavid Monniaux2020-03-035-784/+213
| |\
| | * CSE2 alias analysis for Risc-VDavid Monniaux2020-03-033-30/+2
| | * moved away x86-dependent partsDavid Monniaux2020-03-031-38/+0
| | * modularize proofDavid Monniaux2020-03-031-29/+10
| | * may_overlap_soundDavid Monniaux2020-03-031-0/+38
| | * starting to move x86 stuff to x86David Monniaux2020-03-031-201/+1
| | * offsets in globals for x86David Monniaux2020-03-032-2/+82
| | * globals alias analysis for x86David Monniaux2020-03-032-10/+59
| | * with indexed/indexed alias analysis for x86David Monniaux2020-03-032-4/+26
| | * kill_store_soundDavid Monniaux2020-03-021-10/+25
| | * kill_store1_soundDavid Monniaux2020-03-021-3/+41
| | * load_store_awayDavid Monniaux2020-03-021-1/+2
| | * swap predicateDavid Monniaux2020-03-022-13/+27
| | * works on x86 x86_64David Monniaux2020-03-021-29/+47
| | * playing with offsetsDavid Monniaux2020-03-021-1/+67
| | * Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naiveDavid Monniaux2020-03-0217-96/+174
| | |\
| | | * Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-021-3/+2
| | | * Define IRC.class_of_type for types Tany32, Tany64Xavier Leroy2020-03-021-1/+2
| * | | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-0368-342/+4246
| |\ \ \
| * | | | CSE2 now uses is_trivial_opDavid Monniaux2020-02-272-3/+22
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2David Monniaux2020-02-2715-92/+170
| |\ \ \ \ | | | |_|/ | | |/| |
| | * | | Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-0/+67
| | * | | Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-212-2/+2
| | * | | Refine the type of function results in AST.signatureXavier Leroy2020-02-2113-90/+101
| * | | | add hintDavid Monniaux2020-02-051-0/+1
| * | | | wellformed_reg_kill_memDavid Monniaux2020-02-051-1/+17
| * | | | rm useless admitted lemmaDavid Monniaux2020-02-051-5/+0
| * | | | wellformed_reg_kill_reg simpliiedDavid Monniaux2020-02-051-8/+3
| * | | | wellformed_reg_kill_regDavid Monniaux2020-02-051-0/+129
| * | | | progress on wellformed regDavid Monniaux2020-02-052-12/+84
| * | | | wellformedness for reg begins; simplifiedDavid Monniaux2020-02-041-12/+9
| * | | | wellformedness for reg beginsDavid Monniaux2020-02-041-0/+53
| * | | | kill memory focusedDavid Monniaux2020-02-042-20/+46
| * | | | invariant guaranteedDavid Monniaux2020-02-042-4/+56
| * | | | wellformedness for memoryDavid Monniaux2020-02-042-17/+158
| * | | | begin well formednessDavid Monniaux2020-02-042-15/+130
| * | | | stuff information into a recordDavid Monniaux2020-02-042-46/+63
| | |_|/ | |/| |
* | | | Linearizeaux: Fixed bug where the output list was in reverse orderCyril SIX2020-03-091-4/+20
* | | | Adding debug info in LinearizeauxCyril SIX2020-03-061-0/+12
* | | | [UNTESTED] Sequence orderingCyril SIX2020-03-061-3/+27
* | | | Linearize: Dependencies computing to decide which sequence to put firstCyril SIX2020-03-031-31/+132
* | | | Linearizeaux: can_be_mergedCyril SIX2020-02-211-13/+48
* | | | Linearizeaux: function try_mergeCyril SIX2020-02-211-11/+20
* | | | WIP2Cyril SIX2020-02-201-16/+24
generated by cgit (git 2.34.1) at 2024-06-12 12:07:52 +0000