aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
* Merge of Flocq version 2.2.0.xleroy2013-08-021-10/+12
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-2/+2
* Updating LICENSE and license headers, continued.xleroy2013-06-171-0/+3
* Fix compilation of runtime system.xleroy2013-05-291-0/+4
* Merge of the float32 branch: xleroy2013-05-191-1/+1
* Preliminary support for debugging info (-g).xleroy2013-05-171-0/+1
* Clean up 'make clean'xleroy2013-05-011-2/+1
* Use "-as" to put CompCert modules in a compcert.xxx namespace.xleroy2013-05-011-7/+16
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-11/+8
* Updated issues with coqchk. See PR#3026 on the Coq bug tracker.xleroy2013-04-141-6/+9
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-1/+1
* 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
generated by cgit (git 2.34.1) at 2024-06-02 21:37:31 +0000