aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
* Support for indirect symbols under MacOS X (final).xleroy2012-07-141-1/+1
* Revert unintentional commit #1955xleroy2012-07-061-6/+6
* Ajout trunk CompCertblazy2012-07-041-6/+6
* Use Flocq for floatsxleroy2012-06-281-2/+14
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-261-1/+1
* Merge of the newmem branch:xleroy2012-05-211-3/+6
* Configuration, build and install for cchecklink. Clean-ups in myocamlbuild.ml.xleroy2012-04-041-1/+7
* checklink: first import of Valentin Robert's validator for asm and linkxleroy2012-03-281-4/+18
* make clean must erase tools/ndfunxleroy2012-03-131-0/+1
* Cosmetic cleanups.xleroy2012-01-151-2/+0
* Merge of the nonstrict-ops branch:xleroy2012-01-141-4/+12
* Changelog, doc: updated for release 1.9v1.9xleroy2011-08-221-0/+7
* New backend pass "RRE": optimize (somewhat) redundant reloads introduced by t...xleroy2011-08-161-0/+1
* ARM codegen ported to new ABI + VFD floatsxleroy2011-07-301-8/+8
* Updated Makefile and dependencies. Typo in powerpc/PrintAsm.ml.xleroy2011-07-281-2/+1
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-281-2/+2
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-1/+2
* Added pass CleanupLabels to remove unreferenced labels in a proved way.xleroy2011-05-081-0/+1
* Renamed Machconcr into Machsem.xleroy2011-04-091-1/+1
* Merge of branch "unsigned-offsets":xleroy2011-04-091-2/+2
* Initializers for global variables: compile-time evaluation of expressions don...xleroy2011-03-121-0/+1
* Revised signed/unsigned char handling.xleroy2011-03-101-1/+0
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-091-1/+0
* Treat "char" as unsigned OR signed depending on the configuration.xleroy2011-03-091-0/+1
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...xleroy2010-10-271-1/+1
* Updates for IA32-Cygwin.xleroy2010-09-081-3/+11
* Simplified stdlib wrapper; use it only under MacOS Xxleroy2010-09-041-1/+2
* Removed useless constraints on return type at Sreturn instructionsxleroy2010-08-181-0/+3
* Merge of branches/full-expr-4:xleroy2010-08-181-2/+4
* Support for inlined built-ins.xleroy2010-06-291-2/+2
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-281-1/+1
* Cleaner generation of .dependxleroy2010-03-301-2/+2
* New HTML documentation generatorxleroy2010-03-091-15/+11
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-2/+2
* Suppressed Init_pointer, now useless. Improved printing of strings in genera...xleroy2010-03-031-0/+1
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-031-9/+1
* Coloringaux: make identifiers unique; special treatment of precolored xleroy2009-08-261-1/+5
* Build bytecode version with debug symbols.xleroy2009-08-201-2/+2
* Refactoring of Constprop and Constpropproof into a machine-dependent part and...xleroy2009-08-171-1/+1
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...xleroy2009-08-171-1/+1
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-1/+1
* Added 'going wrong' behaviorsxleroy2009-08-051-1/+1
* Various clean-upsv1.4xleroy2009-04-171-10/+27
* Added tail call optimization passxleroy2009-03-261-0/+1
* make install: ./ccomp au lieu de ../ccompblazy2009-02-271-1/+2
* Updatesxleroy2009-01-051-2/+9
* Wrong dependenciesxleroy2009-01-021-4/+6
* Continuation of ARM port.xleroy2009-01-011-7/+16
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-19/+40
* Revu removeproofxleroy2008-03-191-1/+8
generated by cgit (git 2.34.1) at 2024-06-02 22:57:38 +0000