summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Merge of the nonstrict-ops branch:Gravatar xleroy2012-01-14
* UpdateGravatar xleroy2011-11-27
* More careful updating of current location for error msgs.Gravatar xleroy2011-11-26
* cparser/*: refactoring of the expansion of read-modify-write operatorsGravatar xleroy2011-11-26
* Fixed serious bug in handling of volatile arrays.Gravatar xleroy2011-11-26
* Interp: accommodate "int main(int, char **)".Gravatar xleroy2011-10-19
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsGravatar xleroy2011-10-18
* Corrected initialization of char arrays by string literals.Gravatar xleroy2011-10-17
* More cleanups in packed struct emulation.Gravatar xleroy2011-10-16
* Revised emulation of packed structsGravatar xleroy2011-10-16
* Watch out for min_int / -1Gravatar xleroy2011-08-27
* Doc fixesGravatar xleroy2011-08-23
* MAJ licenceGravatar xleroy2011-08-23
* Changelog, doc: updated for release 1.9Gravatar xleroy2011-08-22
* arm/PrintAsm: don't generate "vfd" directive, useless?Gravatar xleroy2011-08-22
* Harden proof script against empty destroyed_at_moveGravatar xleroy2011-08-22
* Wrong check: &e must be rejected if e has array type and is not a l-value.Gravatar xleroy2011-08-21
* Cleaned up old commented-out partsGravatar xleroy2011-08-19
* More careful treatment of 'load immediate 0' as 'xor self'Gravatar xleroy2011-08-18
* Presimplification SimplVolatile: cleaned up and integrated.Gravatar xleroy2011-08-18
* SimplVolatile: new pass to eliminate read-modify-write ops over volatilesGravatar xleroy2011-08-18
* Factor out bind_lvalueGravatar xleroy2011-08-17
* MAJGravatar xleroy2011-08-16
* New backend pass "RRE": optimize (somewhat) redundant reloads introduced by t...Gravatar xleroy2011-08-16
* Forgot to update: adding xchg instructionGravatar xleroy2011-08-16
* Locations.v: add Loc.diff_dec.Gravatar xleroy2011-08-14
* IA32 PrintAsm.ml: wrong moves generated in print_builtin_memcpy_bigGravatar xleroy2011-08-10
* IA32: wrong moves generated in print_builtin_memcpy_big.Gravatar xleroy2011-08-10
* Treatment of volatiles: offer the choice between random reads and treating vo...Gravatar xleroy2011-08-09
* More vigorous scrubbing of r-value structsGravatar xleroy2011-08-09
* Improved treatment of structs/unions as r-valuesGravatar xleroy2011-08-08
* IA32 port: more faithful treatment of pseudoregister ST0.Gravatar xleroy2011-08-08
* Cleaned up handling of composite conditionsGravatar xleroy2011-08-05
* Wrong ifdef PPCGravatar xleroy2011-08-05
* More builtins for ARM and PowerPCGravatar xleroy2011-08-05
* arm/PrintAsm: bugs in expansion of new builtinsGravatar xleroy2011-08-05
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 19:14:29 +0000