aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
Commit message (Expand)AuthorAgeFilesLines
...
* Assorted fixes to fix parsing issues and be more GCC-like:xleroy2014-05-121-3/+2
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-1/+25
* Clean-up pass on C types:xleroy2014-04-231-0/+2
* Merge of branch linear-typing:xleroy2014-04-061-0/+2
* In Regalloc, dead code elimination, don't eliminate move operationsxleroy2014-02-231-1/+1
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-12/+12
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-8/+4
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-10/+1
* Merge of branch value-analysis.xleroy2013-12-201-5/+11
* Revised semantics of external functions, continued:xleroy2013-11-181-4/+0
* Revised modeling of external functions and built-in functions: just axiomatizexleroy2013-11-171-0/+4
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms xleroy2013-09-141-3/+3
* Merge of Flocq version 2.2.0.xleroy2013-08-021-3/+7
* Add option -fno-tailcalls to turn off tailcall elimination (causes problem wi...xleroy2013-05-171-0/+5
* Oops, removed a crucial declaration for Allocation.xleroy2013-05-011-0/+4
* Coq-defined equality functions for Allocation.xleroy2013-05-011-11/+0
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-5/+31
* RTLtyping: now performed entirely in Coq, no need for an external Caml oracle...xleroy2013-03-221-3/+0
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-1/+10
* Merge of the clightgen branch:xleroy2012-12-291-1/+1
* Support for indirect symbols under MacOS X (final).xleroy2012-07-141-1/+2
* Support for MacOS X's indirect symbols. (first try)xleroy2012-07-131-2/+2
* Use Flocq for floatsxleroy2012-06-281-21/+7
* Merge of the newmem branch:xleroy2012-05-211-2/+17
* Merge of the nonstrict-ops branch:xleroy2012-01-141-1/+0
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-5/+2
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-281-1/+0
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).xleroy2011-05-081-0/+1
* Initializers for global variables: compile-time evaluation of expressions don...xleroy2011-03-121-1/+1
* Undesirable optimization of 'print'xleroy2011-03-101-0/+2
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-093-32/+8
* float->int conversions, continued: weaker axiomatization.xleroy2010-10-291-1/+0
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-0/+1
* Merge of the reuse-temps branch:xleroy2010-09-021-1/+0
* Merge of branches/full-expr-4:xleroy2010-08-181-0/+11
* Revised encoding/decoding of floatsxleroy2010-05-091-2/+4
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-0/+8
* Updated ARM portxleroy2010-01-251-4/+0
* PowerPC/EABI port: preliminary support for #pragma section andxleroy2009-11-031-9/+4
* Simplified the treatment of the PowerPC small data area; now more specific to...xleroy2009-11-021-1/+0
* Preliminary support for small data area in PowerPC port.xleroy2009-11-011-0/+3
* Updated Selectionxleroy2009-08-181-1/+1
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-161-33/+14
* Use Extraction Blacklistxleroy2009-07-253-17/+3
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-052-20/+16
* Various clean-upsv1.4xleroy2009-04-174-54/+17
* Update creation Configuration.mlxleroy2009-03-291-1/+2
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...xleroy2009-01-292-12/+12
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-304-646/+26
* Extract Coq lists to Caml lists.xleroy2008-12-292-2/+4
generated by cgit (git 2.34.1) at 2024-05-20 02:55:23 +0000