aboutsummaryrefslogtreecommitdiffstats
path: root/.depend
Commit message (Expand)AuthorAgeFilesLines
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-0/+172
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-19/+21
* Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-061-31/+32
* Upgrade to Flocq 2.5.0.Guillaume Melquiond2015-09-221-4/+4
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-3/+5
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-3/+3
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-211-7/+7
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-171-9/+9
* Missing initialization of current_function_sig.Xavier Leroy2015-03-141-2/+2
* Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-311-8/+9
* Verification of the Unusedglob pass (removal of unreferenced static global de...Xavier Leroy2014-11-241-1/+3
* Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0.Xavier Leroy2014-10-091-0/+1
* Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-071-2/+2
* Update dependenciesxleroy2014-08-191-14/+14
* Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.xleroy2014-07-231-7/+7
* Merge of "newspilling" branch:xleroy2014-07-231-11/+12
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-0/+13
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...xleroy2014-04-091-7/+7
* Merge of branch linear-typing:xleroy2014-04-061-10/+10
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-281-10/+10
* Move wt_instr_inv where it belongs.xleroy2014-03-271-10/+10
* Force dependency of SelectOp on Compopts.xleroy2014-03-031-1/+1
* Remove useless checks on type_of_global in dynamic semanticsxleroy2014-02-201-10/+10
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-12/+13
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-7/+7
* Merge of branch value-analysis.xleroy2013-12-201-9/+18
* Merge of the "alignas" branch.xleroy2013-10-051-1/+1
* Merge of Flocq version 2.2.0.xleroy2013-08-021-18/+20
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-2/+4
* Merge of the float32 branch: xleroy2013-05-191-1/+2
* Use "-as" to put CompCert modules in a compcert.xxx namespace.xleroy2013-05-011-7/+7
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-37/+23
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-5/+6
* No longer a dependency on Machtypingxleroy2013-03-011-1/+1
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-10/+7
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-150/+150
* More correct exportclight/ dependenciesxleroy2013-01-081-6/+7
* Remove some useless "Require".xleroy2012-12-301-64/+64
* Merge of the clightgen branch:xleroy2012-12-291-0/+2
* Clight: split off the big step semantics in ClightBigstep.xleroy2012-10-141-0/+1
* Make Clight independent of CompCert C.xleroy2012-10-081-12/+14
* Update CombineOp for arm and ia32.xleroy2012-07-031-3/+3
* Changelog: updatedxleroy2012-06-281-4/+4
* Use Flocq for floatsxleroy2012-06-281-2/+29
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-261-4/+6
* Merge of the newmem branch:xleroy2012-05-211-3/+10
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-2/+2
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-231-5/+5
* Cosmetic cleanups.xleroy2012-01-151-4/+4
* Merge of the nonstrict-ops branch:xleroy2012-01-141-7/+5
generated by cgit (git 2.34.1) at 2024-06-02 14:24:42 +0000