summaryrefslogtreecommitdiff
path: root/cfrontend/C2C.ml
Commit message (Expand)AuthorAge
...
* Initializers: handle By_copy accesses (e.g. for &(glob.field))Gravatar xleroy2012-02-07
* Merge of the "volatile" branch:Gravatar xleroy2012-02-04
* More careful updating of current location for error msgs.Gravatar xleroy2011-11-26
* Fixed serious bug in handling of volatile arrays.Gravatar xleroy2011-11-26
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsGravatar xleroy2011-10-18
* Corrected initialization of char arrays by string literals.Gravatar xleroy2011-10-17
* MAJ licenceGravatar xleroy2011-08-23
* arm/PrintAsm: don't generate "vfd" directive, useless?Gravatar xleroy2011-08-22
* Presimplification SimplVolatile: cleaned up and integrated.Gravatar xleroy2011-08-18
* Flag long long and long double literalsGravatar xleroy2011-07-31
* Added animation of the CompCert C semantics (ccomp -interp)Gravatar xleroy2011-07-28
* Revised handling of annotation statements, and more generally built-in functi...Gravatar xleroy2011-06-13
* cparser: support for attributes over struct and union.Gravatar xleroy2011-05-12
* cparser/StructAssign: always use __builtin_memcpy + alignment indicationGravatar xleroy2011-05-11
* Preliminary support for 'aligned' and 'section' attributes, gcc-style. New-s...Gravatar xleroy2011-04-16
* More global initialization work done and proved in Coq.Gravatar xleroy2011-03-13
* Initializers for global variables: compile-time evaluation of expressions don...Gravatar xleroy2011-03-12
* Revised signed/unsigned char handling.Gravatar xleroy2011-03-10
* Treat "char" as unsigned OR signed depending on the configuration.Gravatar xleroy2011-03-09
* Updates for IA32-Cygwin.Gravatar xleroy2010-09-08
* Better emulation of long long as a struct.Gravatar xleroy2010-09-04
* Adding __builtin_annotationGravatar xleroy2010-09-01
* Copyright bannerGravatar xleroy2010-08-18
* Renamed C2Clight into C2CGravatar xleroy2010-08-18