aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Expand)AuthorAgeFilesLines
* Updates for IA32-Cygwin.xleroy2010-09-081-20/+31
* Better emulation of long long as a struct.xleroy2010-09-041-15/+50
* Adding __builtin_annotationxleroy2010-09-012-1/+112
* Nettoyages pour docxleroy2010-08-183-20/+14
* Removed useless constraints on return type at Sreturn instructionsxleroy2010-08-187-36/+25
* Copyright bannerxleroy2010-08-181-0/+12
* Renamed C2Clight into C2Cxleroy2010-08-181-0/+0
* Merge of branches/full-expr-4:xleroy2010-08-1819-5551/+10763
* Support for inlined built-ins.xleroy2010-06-297-103/+131
* Updated Caml parts to match new representation for global variables.xleroy2010-05-262-12/+27
* More faithful semantics for volatile reads and writes.xleroy2010-05-236-32/+40
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-104-67/+73
* Suppressed axioms Float.eq_zero_{true,false}, since the latter isxleroy2010-05-092-11/+8
* Cleaned up handling of linker sections.xleroy2010-05-081-14/+13
* Strengthen chunktype inference and use it to remove some useless casts.xleroy2010-05-052-23/+141
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-026-3/+39
* __builtin_memcpy, continued.xleroy2010-04-171-3/+3
* Support __builtin_memcpy; use it for struct assignmentxleroy2010-04-171-0/+13
* PowerPC: xleroy2010-04-101-0/+7
* Bug fix: infinite loop in cparser/ on bit field of size 32 bits.xleroy2010-04-091-4/+2
* Wrong type for __builtin_volatile_*_int32xleroy2010-04-021-1/+1
* Typoxleroy2010-03-281-1/+0
* Bug in multidimensional read-only arraysxleroy2010-03-131-7/+8
* Handling of volatile accesses through builtin functions.xleroy2010-03-081-18/+105
* Handling of builtins, continued.xleroy2010-03-072-29/+42
* Merge of the newmem and newextcalls branches:xleroy2010-03-078-1296/+1957
* Suppressed Init_pointer, now useless. Improved printing of strings in genera...xleroy2010-03-031-4/+0
* Detect struct assignment. Silence some warningsxleroy2010-03-031-3/+7
* Getting rid of CILxleroy2010-03-031-1283/+0
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-034-0/+768
* Function types didn't always degrade to pointers like they should. Introduce...xleroy2010-03-024-23/+26
* Revised handling of #pragma section and small data areasxleroy2010-01-271-17/+21
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-192-6/+6
* Unsupported: return/return type mismatchesxleroy2009-11-191-2/+17
* PowerPC/EABI port: preliminary support for #pragma section andxleroy2009-11-031-50/+47
* Simplified the treatment of the PowerPC small data area; now more specific to...xleroy2009-11-021-10/+8
* Preliminary support for small data area in PowerPC port.xleroy2009-11-011-0/+15
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-012-7/+21
* Problem with const enum initializersxleroy2009-09-151-0/+2
* Last updates for release 1.5.v1.5xleroy2009-08-281-9/+9
* Stronger constant folding, esp. w.r.t. floatsxleroy2009-08-211-40/+158
* In generated Cminor functions, make sure local variables includexleroy2009-08-202-23/+100
* No '\n' in Coq strings...xleroy2009-08-181-1/+1
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-162-64/+170
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-162-29/+46
* Added 'going wrong' behaviorsxleroy2009-08-052-7/+8
* Transition semantics for Clight and Csharpminorxleroy2009-08-0310-2342/+2996
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-057-148/+149
* Various clean-upsv1.4xleroy2009-04-171-5/+5
* Honor "static" modifier on C globals.xleroy2009-03-281-10/+44
generated by cgit (git 2.34.1) at 2024-06-12 13:44:21 +0000