aboutsummaryrefslogtreecommitdiffstats
path: root/.depend
Commit message (Expand)AuthorAgeFilesLines
* 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
* New backend pass "RRE": optimize (somewhat) redundant reloads introduced by t...xleroy2011-08-161-1/+4
* Locations.v: add Loc.diff_dec.xleroy2011-08-141-3/+3
* Updated Makefile and dependencies. Typo in powerpc/PrintAsm.ml.xleroy2011-07-281-3/+4
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-281-2/+3
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-4/+4
* Added pass CleanupLabels to remove unreferenced labels in a proved way.xleroy2011-05-081-1/+4
* Renamed Machconcr into Machsem.xleroy2011-04-091-5/+5
* Merge of branch "unsigned-offsets":xleroy2011-04-091-9/+7
* Initializers for global variables: compile-time evaluation of expressions don...xleroy2011-03-121-102/+104
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...xleroy2010-10-271-4/+5
* Merge of the reuse-temps branch:xleroy2010-09-021-2/+2
* Merge of branches/full-expr-4:xleroy2010-08-181-8/+12
* Support for inlined built-ins.xleroy2010-06-291-31/+32
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-281-7/+8
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-1/+1
* Strengthen chunktype inference and use it to remove some useless casts.xleroy2010-05-051-1/+1
* Cleaner generation of .dependxleroy2010-03-301-67/+63
generated by cgit (git 2.34.1) at 2024-06-02 15:19:45 +0000