summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* 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
* - Extended traces so that pointers within globals are supported as event values.Gravatar xleroy2010-05-10
* Another regressionGravatar xleroy2010-05-10
* Fewer float axioms.Gravatar xleroy2010-05-09
* Suppressed axioms Float.eq_zero_{true,false}, since the latter isGravatar xleroy2010-05-09
* Revised encoding/decoding of floatsGravatar xleroy2010-05-09
* Cleaned up handling of linker sections.Gravatar xleroy2010-05-08
* Improved coalescing heuristics based on Hailperin's paper.Gravatar xleroy2010-05-08
* Cosmetic: comments to mark expansions of some pseudoinstructions.Gravatar xleroy2010-05-08
* UpdateGravatar xleroy2010-05-05
* Strengthen chunktype inference and use it to remove some useless casts.Gravatar xleroy2010-05-05
* More theorems about sign and zero extensionsGravatar xleroy2010-05-05
* Removed an ADMITTED that was unused, fortunatelyGravatar xleroy2010-05-05
* Pretty-printers for RTL and LTL. Not yet well integrated.Gravatar xleroy2010-05-02
* Compute spill costs.Gravatar xleroy2010-05-02
* In compilation of Sassign, avoid systematic move from a fresh temp.Gravatar xleroy2010-05-02
* Add "fabs" (floating-point absolute value) as a unary operator inGravatar xleroy2010-05-02
* Optimisation: addrsymbol + (expr + cst) and addrstack + (expr + cst).Gravatar xleroy2010-05-02
* ARM version of MachregsauxGravatar xleroy2010-05-01
* More struct testsGravatar xleroy2010-04-17
* __builtin_memcpy, continued.Gravatar xleroy2010-04-17
* Support __builtin_memcpy; use it for struct assignmentGravatar xleroy2010-04-17
* Update for 1.7.1Gravatar xleroy2010-04-13
* PowerPC: Gravatar xleroy2010-04-10
* Coloring: allow to exclude user-specified registers from allocation.Gravatar xleroy2010-04-10
* Test bit field of size 32Gravatar xleroy2010-04-09
* Bug fix: infinite loop in cparser/ on bit field of size 32 bits.Gravatar xleroy2010-04-09
* Static initialization of structs with bitfieldsGravatar xleroy2010-04-07
* Wrong type for __builtin_volatile_*_int32Gravatar xleroy2010-04-02
* In cparser/SimplExpr.ml:Gravatar xleroy2010-04-02
* cparser/AddCasts.ml: forgot to materialize cast at return statement.Gravatar xleroy2010-04-01
* Updates for release 1.7Gravatar xleroy2010-03-30
* Update for 1.7Gravatar xleroy2010-03-30
* Determine endianness at run-timeGravatar xleroy2010-03-30
* Options -I -D -U with a spaceGravatar xleroy2010-03-30