summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* Undesirable optimization of 'print'Gravatar xleroy2011-03-10
* Bitfields: MSB-to-LSB in addition to LSB-to-MSBGravatar xleroy2011-03-10
* Revised signed/unsigned char handling.Gravatar xleroy2011-03-10
* Improved test harnessGravatar xleroy2011-03-10
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.Gravatar xleroy2011-03-09
* Treat "char" as unsigned OR signed depending on the configuration.Gravatar xleroy2011-03-09
* Use movapd instead of movsd for xmm reg-reg move: it avoids partial register ...Gravatar xleroy2010-11-28
* In StructAssign: be careful not to duplicate accesses to a volatile variable.Gravatar xleroy2010-11-10
* float->int conversions, continued: weaker axiomatization.Gravatar xleroy2010-10-29
* Float.intoffloat and Float.intuoffloat are now partial functions.Gravatar xleroy2010-10-28
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...Gravatar xleroy2010-10-27
* License for Floataux.mlGravatar xleroy2010-10-27
* Inconsistent treatment of "lone" zero-width bit fieldsGravatar xleroy2010-09-24
* Bizarre use of struct valueGravatar xleroy2010-09-21
* Update for release 1.8Gravatar xleroy2010-09-21
* Typo in doc commentGravatar xleroy2010-09-21
* Memory.v: added drop_perm operationGravatar xleroy2010-09-21
* No crash if nonexistent input file.Gravatar xleroy2010-09-14
* CommentsGravatar xleroy2010-09-10
* Improvements for int8 and int16 storesGravatar xleroy2010-09-10
* Updates for IA32-Cygwin.Gravatar xleroy2010-09-08
* UpdatedGravatar xleroy2010-09-04
* ++ on volatile not supported.Gravatar xleroy2010-09-04
* Update: adding __builtin_annotationGravatar xleroy2010-09-04
* Simplified stdlib wrapper; use it only under MacOS XGravatar xleroy2010-09-04
* Support for __builtin_fmax and __builtin_fminGravatar xleroy2010-09-04
* Better emulation of long long as a struct.Gravatar xleroy2010-09-04
* Merge of the reuse-temps branch:Gravatar xleroy2010-09-02
* Semantics of annotationsGravatar xleroy2010-09-02
* Adding __builtin_annotationGravatar xleroy2010-09-01
* Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of readi...Gravatar xleroy2010-09-01
* Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_extGravatar xleroy2010-08-21
* 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
* Wrong cast in constant_exprGravatar xleroy2010-08-04
* Fix extraction problemGravatar xleroy2010-07-14
* Preliminary support for gcc-style __attribute__ over typesGravatar xleroy2010-07-08
* Bug in cparser/AddCasts.ml.Gravatar xleroy2010-07-08
* Render unto Caesar... (Mention contribution by Dockins and Steward.)Gravatar xleroy2010-07-08
* Forgot to add this file. Part of the refactoring of $ARCH/$SYSTEM/Conventions.vGravatar xleroy2010-07-07
* Support for inlined built-ins.Gravatar xleroy2010-06-29
* All axioms used in the CompCert developmentGravatar xleroy2010-06-28
* Merging the Princeton implementation of the memory model. Separate axioms in...Gravatar xleroy2010-06-28
* Updated Caml parts to match new representation for global variables.Gravatar xleroy2010-05-26
* Clean upGravatar xleroy2010-05-26
* Typo in documentationGravatar xleroy2010-05-26
* More faithful semantics for volatile reads and writes.Gravatar xleroy2010-05-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 13:34:11 +0000