aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-4/+3
* More correct exportclight/ dependenciesxleroy2013-01-081-2/+2
* Put clighgen files in exportclight/xleroy2013-01-051-7/+10
* RTLgenaux: heuristic to orient if-then-else statements based on sizes.xleroy2012-12-311-2/+4
* Make "all" the defaut target.xleroy2012-12-291-18/+21
* Merge of the clightgen branch:xleroy2012-12-291-2/+11
* Clight: split off the big step semantics in ClightBigstep.xleroy2012-10-141-1/+1
* Make Clight independent of CompCert C.xleroy2012-10-081-1/+1
* 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
generated by cgit (git 2.34.1) at 2024-06-11 18:32:49 +0000