aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
Commit message (Expand)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* Conditions now propagated by CSE3David Monniaux2021-01-201-1/+3
|\
| * begin implementing -fcse3-conditionsDavid Monniaux2020-12-091-0/+2
| * CSE3 with Abst_sameDavid Monniaux2020-12-081-1/+1
| * CSE3 now runs on its own fixpoint iterator not based on Kildall.vDavid Monniaux2020-12-081-1/+1
| * passage à EquDavid Monniaux2020-11-261-1/+1
* | fix extraction of non-aarch64 targetsSylvain Boulmé2020-12-171-2/+0
* | Removing OrigAsmgen by moving the necessary functions in Asmgen.v Léo Gourdin2020-11-251-1/+3
* | Merge remote-tracking branch 'origin/aarch64_Pfmovimm_fix' into aarch64-postpassLéo Gourdin2020-11-181-0/+2
|\|
| * in CSE3 choose lowest variable as representative for movesDavid Monniaux2020-10-291-0/+2
* | aarch64 compiles again (but ccomp generates incorrect assembly)Sylvain Boulmé2020-10-231-1/+3
|/
* Changing duplicate verifier to be non optionalCyril SIX2020-10-091-2/+0
* -fcse3-glbDavid Monniaux2020-05-061-0/+2
* CSE3 across mergesDavid Monniaux2020-05-061-0/+2
* Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-231-0/+2
|\
| * CSE3 across callsDavid Monniaux2020-04-231-0/+2
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-201-1/+10
|\|
| * add options for controlling madd and notrap selectionDavid Monniaux2020-04-191-0/+2
| * forgotten extractionDavid Monniaux2020-04-191-1/+2
| * route through LICMauxDavid Monniaux2020-04-011-0/+3
| * begin adapting for LICM phaseDavid Monniaux2020-04-011-0/+3
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-licmDavid Monniaux2020-04-011-0/+2
| |\
* | \ Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-1/+13
|\ \ \
| * | | reloading and exploiting seems to workDavid Monniaux2020-04-081-1/+6
| * | | print hashesDavid Monniaux2020-04-081-0/+2
| * | | installed Profiling (not finished)David Monniaux2020-04-081-1/+6
| | |/ | |/|
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-04-011-0/+2
|\| | | |/ |/|
| * -fduplicate -1 really desactivates the pass in Coq nowCyril SIX2020-04-011-0/+2
* | CSE3 alias analysisDavid Monniaux2020-03-141-0/+2
* | removed second analysis phaseDavid Monniaux2020-03-121-1/+1
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-111-2/+0
|\|
| * [BROKEN] Replacing the boolean -fduplicate option by an integerCyril SIX2020-03-091-2/+0
* | printing created hashesDavid Monniaux2020-03-101-1/+1
* | starts compiling but still fakeDavid Monniaux2020-03-101-2/+7
* | just the analysisDavid Monniaux2020-03-051-2/+2
* | more about extraction and linkingDavid Monniaux2020-03-051-0/+7
|/
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-061-0/+2
|\
| * Added a flag to desactivate tail duplicationCyril SIX2020-01-271-0/+2
* | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-281-0/+2
|\ \ | |/ |/|
| * connected (just a silly problem)David Monniaux2020-01-281-0/+2
* | connect forward-moves to compilerDavid Monniaux2020-01-081-0/+2
* | to v3.6David Monniaux2019-09-201-1/+1
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-201-0/+1
|\ \
| * | Timings for Machblockgen, Asmblockgen and postpass schedulingCyril SIX2019-09-181-0/+1
* | | -fall-loads-nontrapDavid Monniaux2019-09-091-0/+4
|/ /
* | various fixesDavid Monniaux2019-07-191-0/+1
* | helpers broke compilationDavid Monniaux2019-07-191-5/+0
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-191-11/+6
|\|
| * Make __builtin_sel available from C source codeXavier Leroy2019-07-171-1/+2
| * New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-11/+1