aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Compiler.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-201-22/+46
|\
| * reordering passesDavid Monniaux2020-04-011-8/+8
| * fix Compiler.vDavid Monniaux2020-04-011-12/+16
| * attempt at compilingDavid Monniaux2020-04-011-12/+24
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-licmDavid Monniaux2020-04-011-5/+5
| |\
| * | nop insertion at entrypointDavid Monniaux2020-03-291-15/+23
* | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-13/+31
|\ \ \
| * | | reloading and exploiting seems to workDavid Monniaux2020-04-081-12/+21
| * | | installed Profiling (not finished)David Monniaux2020-04-081-12/+21
| | |/ | |/|
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-04-011-5/+5
|\| | | |/ |/|
| * -fduplicate -1 really desactivates the pass in Coq nowCyril SIX2020-04-011-5/+5
* | typing and store stuffDavid Monniaux2020-03-121-3/+3
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-111-5/+5
|\|
| * [BROKEN] Replacing the boolean -fduplicate option by an integerCyril SIX2020-03-091-5/+5
* | starts compiling but still fakeDavid Monniaux2020-03-101-9/+17
* | CSE3 generate lists of killableDavid Monniaux2020-03-051-1/+1
* | streamlined lattice codeDavid Monniaux2020-03-051-0/+1
|/
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-061-5/+6
|\
| * Added a flag to desactivate tail duplicationCyril SIX2020-01-271-5/+6
* | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-281-9/+18
|\ \ | |/ |/|
| * connected (just a silly problem)David Monniaux2020-01-281-4/+32
* | connect forward-moves to compilerDavid Monniaux2020-01-081-5/+14
* | finish mergeDavid Monniaux2019-12-021-31/+19
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-5/+25
|\ \
| * \ Merge branch 'mppa-work' into mppa-duplicate-rtlCyril SIX2019-10-021-1/+1
| |\ \
| * | | Stubs for Duplicate passCyril SIX2019-09-031-28/+36
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-201-1/+1
|\ \ \ \ | | |/ / | |/| |
| * | | Timings for Machblockgen, Asmblockgen and postpass schedulingCyril SIX2019-09-181-1/+1
| |/ /
* / / -fall-loads-nontrapDavid Monniaux2019-09-091-2/+11
|/ /
* | Compiles for x86 and mppa_k1c (except Asmexpandaux.ml)Sylvain Boulmé2018-11-271-1/+1
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-261-1/+1
* | Rajout d'un return_address_offset. Besoin de changer forward_simu de mach mac...Cyril SIX2018-09-061-1/+1
|/
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-6/+6
* Use "Local" as prefixXavier Leroy2017-02-131-1/+1
* Strengthen the main compiler correctness results to account for separate comp...Xavier Leroy2016-03-061-149/+250
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-24/+24
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-1/+7
* Verification of the Unusedglob pass (removal of unreferenced static global de...Xavier Leroy2014-11-241-1/+8
* Add flags to control individual optimization passes + flag -O0 for turning th...Xavier Leroy2014-11-161-24/+74
* Merge of branch linear-typing:xleroy2014-04-061-22/+25
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-12/+9
* Merge of branch value-analysis.xleroy2013-12-201-1/+8
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-42/+9
* Partial backtracking on previous commit: the "hole in Mach stack frame" xleroy2013-03-031-1/+2
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-5/+0
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-6/+6
* Remove some useless "Require".xleroy2012-12-301-3/+0
* Merge of the clightgen branch:xleroy2012-12-291-4/+9
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-97/+0
* Merge of the newmem branch:xleroy2012-05-211-61/+70
generated by cgit (git 2.34.1) at 2024-07-04 02:13:29 +0000