summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Flag long long and long double literalsGravatar xleroy2011-07-31
* Check fcmpd semanticsGravatar xleroy2011-07-31
* ARM: added reversed load/store builtins + bswap builtin (to be tested)Gravatar xleroy2011-07-30
* ARM codegen ported to new ABI + VFD floatsGravatar xleroy2011-07-30
* Interp.ml: initialize PRNGGravatar xleroy2011-07-29
* Typo in arm/PrintAsm.mlGravatar xleroy2011-07-28
* Updated Makefile and dependencies. Typo in powerpc/PrintAsm.ml.Gravatar xleroy2011-07-28
* Added animation of the CompCert C semantics (ccomp -interp)Gravatar xleroy2011-07-28
* Check for duplicate label definitionsGravatar xleroy2011-07-18
* More precise typechecking of statementsGravatar xleroy2011-07-17
* Improved semantics of castsGravatar xleroy2011-07-17
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the...Gravatar xleroy2011-07-16
* Merge of branch new-semantics: revised and strengthened top-level statements ...Gravatar xleroy2011-07-15
* Fix treatment of function pointers at function calls in the CompCert C and Cl...Gravatar xleroy2011-07-14
* Back from Oregon commit. Gravatar xleroy2011-07-05
* Relating neg and notGravatar xleroy2011-06-22
* Forgot to print Oroli opGravatar xleroy2011-06-22
* Recognition of rlwimi instruction (useful for bitfield assignment)Gravatar xleroy2011-06-21
* Coloringaux: better cost estimate for annotation builtinsGravatar xleroy2011-06-14
* Add preference for annot_val builtinGravatar xleroy2011-06-14
* Forgot to add new fileGravatar xleroy2011-06-14
* Revised handling of annotation statements, and more generally built-in functi...Gravatar xleroy2011-06-13
* Minor update in Clight (big-step)Gravatar blazy2011-06-08
* Oaddrsymbol and small data areaGravatar xleroy2011-06-07
* Ajout big-step Clight et preuve big-step -> small-stepGravatar blazy2011-05-25
* Forgot somethingGravatar xleroy2011-05-24
* Update for release 1.8.2Gravatar xleroy2011-05-24
* Nicer printing of annotations.Gravatar xleroy2011-05-23
* Silence a warning that happens all too often in MacOS XGravatar xleroy2011-05-12
* Another try for the ifdefGravatar xleroy2011-05-12
* Wrong ifdefGravatar xleroy2011-05-12
* TypoGravatar xleroy2011-05-12
* cparser: support for attributes over struct and union.Gravatar xleroy2011-05-12
* cparser/StructAssign: always use __builtin_memcpy + alignment indicationGravatar xleroy2011-05-11
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).Gravatar xleroy2011-05-08
* Added pass CleanupLabels to remove unreferenced labels in a proved way.Gravatar xleroy2011-05-08
* Support compile-time constant expressions as arguments to gcc-style attributesGravatar xleroy2011-04-20
* TyposGravatar xleroy2011-04-19
* Fixed some typos.Gravatar xleroy2011-04-17
* Use memcpy_word only if alignment AND size are multiples of word size.Gravatar xleroy2011-04-17
* Fixed some typosGravatar xleroy2011-04-16
* cparser/Elab: __attribute, not attributeGravatar xleroy2011-04-16
* Preliminary support for 'aligned' and 'section' attributes, gcc-style. New-s...Gravatar xleroy2011-04-16
* Revised handling of GCC attributes. Preliminary, untested support for __alig...Gravatar xleroy2011-04-14
* Renamed Machconcr into Machsem.Gravatar xleroy2011-04-09
* Merge of branch "unsigned-offsets":Gravatar xleroy2011-04-09
* Revised handling of sizeof(string-literal)Gravatar xleroy2011-03-15
* Special case for while(1), for(..., 1, ...) and do ... while(0) loops.Gravatar xleroy2011-03-15
* Update for 1.8.1Gravatar xleroy2011-03-14
* Update for 1.8.1 releaseGravatar xleroy2011-03-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 10:17:51 +0000