aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
* Compute spill costs.xleroy2010-05-021-8/+92
* In compilation of Sassign, avoid systematic move from a fresh temp.xleroy2010-05-023-105/+211
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-027-5/+39
* Optimisation: addrsymbol + (expr + cst) and addrstack + (expr + cst).xleroy2010-05-022-0/+28
* ARM version of Machregsauxxleroy2010-05-012-0/+59
* More struct testsxleroy2010-04-171-1/+2
* __builtin_memcpy, continued.xleroy2010-04-177-20/+117
* Support __builtin_memcpy; use it for struct assignmentxleroy2010-04-175-30/+93
* Update for 1.7.1v1.7.1xleroy2010-04-131-0/+17
* PowerPC: xleroy2010-04-103-3/+32
* Coloring: allow to exclude user-specified registers from allocation.xleroy2010-04-105-28/+131
* Test bit field of size 32xleroy2010-04-093-1/+18
* Bug fix: infinite loop in cparser/ on bit field of size 32 bits.xleroy2010-04-0910-59/+53
* Static initialization of structs with bitfieldsxleroy2010-04-073-1/+109
* Wrong type for __builtin_volatile_*_int32xleroy2010-04-021-1/+1
* In cparser/SimplExpr.ml:xleroy2010-04-024-12/+30
generated by cgit (git 2.34.1) at 2024-07-01 05:28:58 +0000