summaryrefslogtreecommitdiff
path: root/cfrontend
Commit message (Expand)AuthorAge
* 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
* Stronger constant folding, esp. w.r.t. floatsGravatar xleroy2009-08-21
* In generated Cminor functions, make sure local variables includeGravatar xleroy2009-08-20
* No '\n' in Coq strings...Gravatar xleroy2009-08-18
* Cil2Csyntax: added goto and labels; added assignment between structsGravatar xleroy2009-08-16
* Distinguish two kinds of nonterminating behaviors: silent divergenceGravatar xleroy2009-08-16
* Added 'going wrong' behaviorsGravatar xleroy2009-08-05
* Transition semantics for Clight and CsharpminorGravatar xleroy2009-08-03
* Adapted to work with Coq 8.2-1Gravatar xleroy2009-06-05
* Various clean-upsGravatar xleroy2009-04-17
* Honor "static" modifier on C globals.Gravatar xleroy2009-03-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 09:15:28 +0000