aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Bizarre use of struct valuev1.8xleroy2010-09-212-2/+2
* Update for release 1.8xleroy2010-09-213-18/+42
* Typo in doc commentxleroy2010-09-211-2/+2
* Memory.v: added drop_perm operationxleroy2010-09-213-46/+427
* No crash if nonexistent input file.xleroy2010-09-142-2/+3
* Commentsxleroy2010-09-101-8/+10
* Improvements for int8 and int16 storesxleroy2010-09-104-11/+53
* Updates for IA32-Cygwin.xleroy2010-09-085-33/+63
* Updatedxleroy2010-09-042-12/+43
* ++ on volatile not supported.xleroy2010-09-041-2/+2
* Update: adding __builtin_annotationxleroy2010-09-041-1/+36
* Simplified stdlib wrapper; use it only under MacOS Xxleroy2010-09-047-278/+76
* Support for __builtin_fmax and __builtin_fminxleroy2010-09-042-1/+22
* Better emulation of long long as a struct.xleroy2010-09-042-16/+51
* Merge of the reuse-temps branch:xleroy2010-09-0289-2579/+12842
* Semantics of annotationsxleroy2010-09-021-5/+69
* Adding __builtin_annotationxleroy2010-09-018-12/+219
* Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of readi...xleroy2010-09-0110-15/+119
* Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_extxleroy2010-08-217-1121/+1148
* Nettoyages pour docxleroy2010-08-184-21/+15
* Removed useless constraints on return type at Sreturn instructionsxleroy2010-08-188-36/+28
* Copyright bannerxleroy2010-08-181-0/+12
* Renamed C2Clight into C2Cxleroy2010-08-184-7/+7
* Merge of branches/full-expr-4:xleroy2010-08-1856-6180/+13619
* Wrong cast in constant_exprxleroy2010-08-041-3/+3
* Fix extraction problemxleroy2010-07-142-4/+4
* Preliminary support for gcc-style __attribute__ over typesxleroy2010-07-086-135/+168
* Bug in cparser/AddCasts.ml.xleroy2010-07-084-4/+22
* Render unto Caesar... (Mention contribution by Dockins and Steward.)xleroy2010-07-081-0/+2
* Forgot to add this file. Part of the refactoring of $ARCH/$SYSTEM/Conventions.vxleroy2010-07-071-0/+251
* Support for inlined built-ins.xleroy2010-06-2977-1302/+1228
* All axioms used in the CompCert developmentxleroy2010-06-281-0/+27
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-2812-308/+546
* Updated Caml parts to match new representation for global variables.xleroy2010-05-265-26/+57
* Clean upxleroy2010-05-261-25/+0
* Typo in documentationxleroy2010-05-261-1/+1
* More faithful semantics for volatile reads and writes.xleroy2010-05-2336-423/+684
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-1032-351/+507
* Another regressionxleroy2010-05-103-1/+10
* Fewer float axioms.xleroy2010-05-092-6/+3
* Suppressed axioms Float.eq_zero_{true,false}, since the latter isxleroy2010-05-093-14/+8
* Revised encoding/decoding of floatsxleroy2010-05-098-231/+261
* Cleaned up handling of linker sections.xleroy2010-05-089-229/+385
* Improved coalescing heuristics based on Hailperin's paper.xleroy2010-05-081-32/+49
* Cosmetic: comments to mark expansions of some pseudoinstructions.xleroy2010-05-081-7/+17
* Updatexleroy2010-05-051-1/+24
* Strengthen chunktype inference and use it to remove some useless casts.xleroy2010-05-053-24/+142
* More theorems about sign and zero extensionsxleroy2010-05-051-0/+100
* Removed an ADMITTED that was unused, fortunatelyxleroy2010-05-051-2/+0
* Pretty-printers for RTL and LTL. Not yet well integrated.xleroy2010-05-024-0/+235
generated by cgit (git 2.34.1) at 2024-05-20 08:58:12 +0000