summaryrefslogtreecommitdiff
path: root/cfrontend
Commit message (Expand)AuthorAge
* Preliminary support for 'aligned' and 'section' attributes, gcc-style. New-s...Gravatar xleroy2011-04-16
* Merge of branch "unsigned-offsets":Gravatar xleroy2011-04-09
* Special case for while(1), for(..., 1, ...) and do ... while(0) loops.Gravatar xleroy2011-03-15
* Incompatibility 8.3 / 8.3pl1Gravatar xleroy2011-03-14
* Slightly nicer semantics for initializationGravatar xleroy2011-03-13
* 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
* Float.intoffloat and Float.intuoffloat are now partial functions.Gravatar xleroy2010-10-28
* 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
* Nettoyages pour docGravatar xleroy2010-08-18
* Removed useless constraints on return type at Sreturn instructionsGravatar xleroy2010-08-18
* Copyright bannerGravatar xleroy2010-08-18
* Renamed C2Clight into C2CGravatar xleroy2010-08-18
* Merge of branches/full-expr-4:Gravatar xleroy2010-08-18
* Support for inlined built-ins.Gravatar xleroy2010-06-29
* Updated Caml parts to match new representation for global variables.Gravatar xleroy2010-05-26
* More faithful semantics for volatile reads and writes.Gravatar xleroy2010-05-23
* - Extended traces so that pointers within globals are supported as event values.Gravatar xleroy2010-05-10
* Suppressed axioms Float.eq_zero_{true,false}, since the latter isGravatar xleroy2010-05-09
* Cleaned up handling of linker sections.Gravatar xleroy2010-05-08
* Strengthen chunktype inference and use it to remove some useless casts.Gravatar xleroy2010-05-05
* Add "fabs" (floating-point absolute value) as a unary operator inGravatar xleroy2010-05-02
* __builtin_memcpy, continued.Gravatar xleroy2010-04-17
* Support __builtin_memcpy; use it for struct assignmentGravatar xleroy2010-04-17
* PowerPC: Gravatar xleroy2010-04-10
* Bug fix: infinite loop in cparser/ on bit field of size 32 bits.Gravatar xleroy2010-04-09
* Wrong type for __builtin_volatile_*_int32Gravatar xleroy2010-04-02
* TypoGravatar xleroy2010-03-28
* Bug in multidimensional read-only arraysGravatar xleroy2010-03-13
* Handling of volatile accesses through builtin functions.Gravatar xleroy2010-03-08
* Handling of builtins, continued.Gravatar xleroy2010-03-07
* Merge of the newmem and newextcalls branches:Gravatar xleroy2010-03-07
* Suppressed Init_pointer, now useless. Improved printing of strings in genera...Gravatar xleroy2010-03-03
* Detect struct assignment. Silence some warningsGravatar xleroy2010-03-03
* Getting rid of CILGravatar xleroy2010-03-03
* Switching to the new C parser/elaborator/simplifierGravatar xleroy2010-03-03
* Function types didn't always degrade to pointers like they should. Introduce...Gravatar xleroy2010-03-02
* Revised handling of #pragma section and small data areasGravatar xleroy2010-01-27
* Revised lib/Integers.v to make it parametric w.r.t. word size.Gravatar xleroy2009-11-19
* Unsupported: return/return type mismatchesGravatar xleroy2009-11-19
* 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
* Support Clight initializers of the form "int * x = &y;".Gravatar xleroy2009-11-01
* Problem with const enum initializersGravatar xleroy2009-09-15
* Last updates for release 1.5.Gravatar xleroy2009-08-28