aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
Commit message (Expand)AuthorAgeFilesLines
...
| * 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
* Merge branch 'named-structs'Xavier Leroy2015-01-231-1/+7
|\
| * Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-311-0/+3
| * Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-1/+4
* | Protect against redefinition of the __i64_xxx helper library functions.Xavier Leroy2015-01-201-6/+0
|/
* Add flags to control individual optimization passes + flag -O0 for turning th...Xavier Leroy2014-11-161-1/+7
* Moved the timing facility to a seperate file.Bernhard Schommer2014-09-291-1/+1
* Add .gitignore files.Xavier Leroy2014-09-211-0/+5
* Rename "-fthumb" option into "-mthumb" for GCC compatibility.xleroy2014-08-191-1/+1
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-2/+3
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-281-0/+1
* ARM port: add support for Thumb2. To be tested.xleroy2014-07-271-0/+2
generated by cgit (git 2.34.1) at 2024-05-09 09:49:22 +0000