aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
Commit message (Expand)AuthorAgeFilesLines
* Added a flag to desactivate tail duplicationCyril SIX2020-01-271-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
| * If-conversion optimizationXavier Leroy2019-06-061-0/+1
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-031-5/+6
|\ \
| * | If-conversion optimizationXavier Leroy2019-05-311-0/+1
| |/
| * Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-5/+5
* | option -faddx (off by default until questions cleared)David Monniaux2019-05-111-4/+6
* | -fcoalesce-memDavid Monniaux2019-05-031-0/+2
* | command line options (still incomplete)David Monniaux2019-05-021-0/+6
* | -fpostpass-ilpDavid Monniaux2019-03-121-3/+1
* | Added a flag for changing the scheduler (not any choice available right now)Cyril SIX2019-03-121-1/+3
* | -O0 will not perform postpass schedulingCyril SIX2019-01-181-1/+4
* | compilation Asmexpandaux both for x86/ and mppa_k1c/Sylvain Boulmé2018-11-281-1/+2
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-261-1/+0
* | Asmblock & cie - ça compileCyril SIX2018-09-061-2/+1
* | Extraction issueCyril SIX2018-09-061-1/+2
* | MPPA - Optimized branch generation for word compare to 0Cyril SIX2018-04-091-87/+0
* | MPPA - 32-bits immediate eq/neq branchesCyril SIX2018-04-041-0/+16
* | MPPA - fixed typos in extraction/debug/Asmgen.mlCyril SIX2018-04-041-3/+2
* | MPPA Added debug pretty printer for transl_instrCyril SIX2018-04-041-0/+31
* | MPPA Moved debug/Asmgen.ml to extraction/debug/Asmgen.mlCyril SIX2018-04-041-0/+167
* | MPPA - The project compiles.Cyril SIX2018-04-041-0/+1
|/
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-051-0/+3
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-071-0/+2
* Pull request #192: improve the printing of Clight intermediate codeXavier Leroy2017-11-221-0/+1
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-1/+1
* Inline fst and snd from Datatypes.Bernhard Schommer2017-02-061-0/+4
* Removed Cabshelper open and avoided shadowing.Bernhard Schommer2017-02-031-1/+1
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-0/+1
* Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-171-0/+7
* Add interference for indirect calls.Bernhard Schommer2016-09-151-2/+3
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-0/+2
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-0/+2
* Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-061-2/+1
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-1/+1
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-4/+0
* Added versions of the tranform_* functions in AST to work with functionsBernhard Schommer2015-10-081-0/+1
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-0/+2
* Ctyping: better typing of conditional expressions.Xavier Leroy2015-05-211-2/+2
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-091-3/+0
* Take asm clobbers into account for determining callee-save registers used.Xavier Leroy2015-04-231-0/+4
generated by cgit (git 2.34.1) at 2024-06-02 20:55:43 +0000