summaryrefslogtreecommitdiff
path: root/cfrontend
Commit message (Expand)AuthorAge
...
* 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
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...Gravatar xleroy2009-01-29
* - Added alignment constraints to memory loads and stores.Gravatar xleroy2009-01-11
* Reorganized the development, modularizing away machine-dependent parts.Gravatar xleroy2008-12-30
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.Gravatar xleroy2008-12-29
* Clight: ajout Econdition, suppression Eindex.Gravatar xleroy2008-09-27
* Fusion partielle de la branche contsem: Gravatar xleroy2008-07-08
* Utilisation de intoffloatu. Ajout du cas int + ptr.Gravatar xleroy2008-05-31
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs v...Gravatar xleroy2008-05-30
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...Gravatar xleroy2008-05-30