aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* forgot an 'Admitted'David Monniaux2020-03-311-1/+1
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-03-312-10/+17
|\
| * Desactivating branch predictions by defaultCyril SIX2020-03-171-7/+11
| * more inliningDavid Monniaux2020-03-151-3/+6
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-03-115-128/+366
|\|
| * Fixed stupid typo bug preventing the prediction update for the RANDOM predictorCyril SIX2020-03-111-1/+1
| * Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-112-125/+360
| |\
| | * Linearizeaux: dumb selector when cycling dependencies are foundCyril SIX2020-03-101-4/+6
| | * Linearizeaux, forgot to visit the rest of the nodes in dfs_visitCyril SIX2020-03-101-22/+26
| | * Some dependencies were not taken into account in tracelinearizeCyril SIX2020-03-101-15/+12
| | * Linearize: More helpful message when tracelinearize failsCyril SIX2020-03-101-4/+12
| | * Bug fix in ftracelinearizeCyril SIX2020-03-101-4/+15
| | * [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
| | |\
| | * | 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
| | * | WIPCyril SIX2020-02-201-0/+26
| | * | First part of Hansen algorithm - build the sequencesCyril SIX2020-02-191-1/+43
| * | | remet is_trivial_op dans CSE2David Monniaux2020-03-112-2/+5
| | |/ | |/|
| * | removing some coqc 8.10 warningsSylvain Boulmé2020-03-091-1/+1
* | | same version as in dm-cse2David Monniaux2020-03-031-24/+24
|/ /
* | 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
|\ \ \ \ | | |_|/ | |/| |
| * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-142-4/+55
| |\ \ \
| | * | | Added option -ftracelinearize which linearizes based on ifnot branchesCyril SIX2020-02-122-4/+55