aboutsummaryrefslogtreecommitdiffstats
path: root/.depend
Commit message (Expand)AuthorAgeFilesLines
* - 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
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-51/+52
* Backtracking on commit 1220v1.6xleroy2010-01-131-3/+6
* MAJ Changesxleroy2009-12-161-2/+0
* Added support for jump tables in back end.xleroy2009-11-101-3/+6
* Refactoring of Constprop and Constpropproof into a machine-dependent part and...xleroy2009-08-171-3/+5
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...xleroy2009-08-171-3/+5
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-4/+6
* Added 'going wrong' behaviorsxleroy2009-08-051-2/+3
* Added tail call optimization passxleroy2009-03-261-1/+3
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-66/+69
* Revised back-end so that only 2 integer registers are reserved for reloading.xleroy2008-12-211-1/+1
* MAJ documentationxleroy2008-07-271-1/+1
* Alignement de la pile dans PrintPPCxleroy2008-04-131-6/+6
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-7/+7
* Ajout de common/Complements.vxleroy2007-08-261-0/+1
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-44/+56
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...xleroy2007-03-021-7/+5
* Petites adaptations pour Coq 8.1gammaxleroy2006-11-111-2/+1
* Ajout de dependances dans extraction/Makefiletristan2006-09-061-1/+1
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-041-59/+59
* Fusion de la branche "traces":xleroy2006-09-041-31/+39
* Initial import of compcertxleroy2006-02-091-0/+64
generated by cgit (git 2.34.1) at 2024-06-02 16:08:53 +0000