summaryrefslogtreecommitdiff
path: root/extraction
Commit message (Expand)AuthorAge
* Rename "-fthumb" option into "-mthumb" for GCC compatibility.Gravatar xleroy2014-08-19
* - Support "switch" statements over 64-bit integersGravatar xleroy2014-08-17
* PowerPC port: refactored the expansion of built-in functions andGravatar xleroy2014-07-28
* ARM port: add support for Thumb2. To be tested.Gravatar xleroy2014-07-27
* Assorted fixes to fix parsing issues and be more GCC-like:Gravatar xleroy2014-05-12
* Integration of Jacques-Henri Jourdan's verified parser.Gravatar xleroy2014-04-29
* Clean-up pass on C types:Gravatar xleroy2014-04-23
* Merge of branch linear-typing:Gravatar xleroy2014-04-06
* In Regalloc, dead code elimination, don't eliminate move operationsGravatar xleroy2014-02-23
* Add option -Os to optimize for code size rather than for execution speed.Gravatar xleroy2014-02-19
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.Gravatar xleroy2014-01-12
* Introduce and use the platform-specific Archi module giving:Gravatar xleroy2014-01-03
* Merge of branch value-analysis.Gravatar xleroy2013-12-20
* Revised semantics of external functions, continued:Gravatar xleroy2013-11-18
* Revised modeling of external functions and built-in functions: just axiomatizeGravatar xleroy2013-11-17
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms Gravatar xleroy2013-09-14
* Merge of Flocq version 2.2.0.Gravatar xleroy2013-08-02
* Add option -fno-tailcalls to turn off tailcall elimination (causes problem wi...Gravatar xleroy2013-05-17
* Oops, removed a crucial declaration for Allocation.Gravatar xleroy2013-05-01
* Coq-defined equality functions for Allocation.Gravatar xleroy2013-05-01
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:Gravatar xleroy2013-04-20
* RTLtyping: now performed entirely in Coq, no need for an external Caml oracle...Gravatar xleroy2013-03-22
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
* Merge of the clightgen branch:Gravatar xleroy2012-12-29
* Support for indirect symbols under MacOS X (final).Gravatar xleroy2012-07-14
* Support for MacOS X's indirect symbols. (first try)Gravatar xleroy2012-07-13
* Use Flocq for floatsGravatar xleroy2012-06-28
* Merge of the newmem branch:Gravatar xleroy2012-05-21
* Merge of the nonstrict-ops branch:Gravatar xleroy2012-01-14
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsGravatar xleroy2011-10-18
* Added animation of the CompCert C semantics (ccomp -interp)Gravatar xleroy2011-07-28
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).Gravatar xleroy2011-05-08
* Initializers for global variables: compile-time evaluation of expressions don...Gravatar xleroy2011-03-12
* Undesirable optimization of 'print'Gravatar xleroy2011-03-10
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.Gravatar xleroy2011-03-09
* float->int conversions, continued: weaker axiomatization.Gravatar xleroy2010-10-29
* Float.intoffloat and Float.intuoffloat are now partial functions.Gravatar xleroy2010-10-28
* Merge of the reuse-temps branch:Gravatar xleroy2010-09-02
* Merge of branches/full-expr-4:Gravatar xleroy2010-08-18
* Revised encoding/decoding of floatsGravatar xleroy2010-05-09
* Merge of the newmem and newextcalls branches:Gravatar xleroy2010-03-07
* Updated ARM portGravatar xleroy2010-01-25
* PowerPC/EABI port: preliminary support for #pragma section andGravatar xleroy2009-11-03
* Simplified the treatment of the PowerPC small data area; now more specific to...Gravatar xleroy2009-11-02
* Preliminary support for small data area in PowerPC port.Gravatar xleroy2009-11-01
* Updated SelectionGravatar xleroy2009-08-18
* Cil2Csyntax: added goto and labels; added assignment between structsGravatar xleroy2009-08-16
* Use Extraction BlacklistGravatar xleroy2009-07-25
* Adapted to work with Coq 8.2-1Gravatar xleroy2009-06-05
* Various clean-upsGravatar xleroy2009-04-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-16 14:38:52 +0000