aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
Commit message (Expand)AuthorAgeFilesLines
* Change preference for new register in allocatorBernhard Schommer2023-03-061-0/+1
* Introduce `struct_layout` functionBernhard Schommer2022-09-031-1/+2
* Upgrade to Flocq 4.1.Guillaume Melquiond2022-04-261-12/+0
* Upgrade to Flocq 4.0.Guillaume Melquiond2022-04-251-1/+6
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* 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
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-5/+5
* 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
* Assorted fixes to fix parsing issues and be more GCC-like:xleroy2014-05-121-3/+2
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-1/+25
* Clean-up pass on C types:xleroy2014-04-231-0/+2
* Merge of branch linear-typing:xleroy2014-04-061-0/+2
* In Regalloc, dead code elimination, don't eliminate move operationsxleroy2014-02-231-1/+1
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-12/+12
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-8/+4
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-10/+1
* Merge of branch value-analysis.xleroy2013-12-201-5/+11
* Revised semantics of external functions, continued:xleroy2013-11-181-4/+0
* Revised modeling of external functions and built-in functions: just axiomatizexleroy2013-11-171-0/+4
generated by cgit (git 2.34.1) at 2024-05-03 22:49:11 +0000