summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Missing case: initialization of a global variable of type _Bool.Gravatar xleroy2013-05-08
* Add interferences at function entry with destroyed_at_function_entry.Gravatar xleroy2013-05-08
* Revised semantics and compilation of 2-argument C operators to better match Gravatar xleroy2013-05-06
* Refactoring: move definition of chunk_of_type to AST.v.Gravatar xleroy2013-05-06
* Syntax errorsGravatar xleroy2013-05-06
* Wrong pseudo-instrGravatar xleroy2013-05-06
* Support for in64 -> float conversions w/ correct rounding.Gravatar xleroy2013-05-06
* ia32/i64_dtou: wrong play on rounding modeGravatar xleroy2013-05-05
* Extend CSE of loads following stores to chunks Mint64 and Mfloat64al32.Gravatar xleroy2013-05-02
* Stack-align to 8 arguments of Tfloat and Tlong types, as per the SVR4 ABI and...Gravatar xleroy2013-05-02
* Clean up 'make clean'Gravatar xleroy2013-05-01
* Use "-as" to put CompCert modules in a compcert.xxx namespace.Gravatar xleroy2013-05-01
* Oops, removed a crucial declaration for Allocation.Gravatar xleroy2013-05-01
* Coq-defined equality functions for Allocation. (continued)Gravatar xleroy2013-05-01
* Coq-defined equality functions for Allocation.Gravatar xleroy2013-05-01
* Removing modules now unusedGravatar xleroy2013-05-01
* Add bswap16Gravatar xleroy2013-04-30
* Updated to Pbuiltin with list of resultsGravatar xleroy2013-04-30
* Updated to new CminorSelGravatar xleroy2013-04-30
* Typos in commentsGravatar xleroy2013-04-30
* UpdatedGravatar xleroy2013-04-30
* Expand 64-bit integer comparisons into 32-bit integer comparisons.Gravatar xleroy2013-04-29
* Decomposing 64-bit "less than" comparisons.Gravatar xleroy2013-04-29
* Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,Gravatar xleroy2013-04-29
* Missing GLOBGravatar xleroy2013-04-23
* Make ia32/ code more portable across systems.Gravatar xleroy2013-04-23
* driver: removed option -flonglongGravatar xleroy2013-04-22
* Results for ARMGravatar xleroy2013-04-22
* Labeled statements inside switch were incorrectly processed.Gravatar xleroy2013-04-22
* Deactivate combination Aindexed 0 / Oadd, as it causes problems with chunk = ...Gravatar xleroy2013-04-21
* Fixes in PowerPC portGravatar xleroy2013-04-21
* Add __builtin_bswap16 and __builtin_bswap32 to all ports.Gravatar xleroy2013-04-20
* Rename arm/linux into arm/eabi, more descriptive.Gravatar xleroy2013-04-20
* Split arch/int64.s into one file per function.Gravatar xleroy2013-04-20
* Configuring the assembler used for the runtime libGravatar xleroy2013-04-20
* Remove __i64_{neg,add,sub,mul}, now handled directly by the compiler.Gravatar xleroy2013-04-20
* Added FFTW benchmark provided by Guillaume MelquiondGravatar xleroy2013-04-20
* Tests "floats" and "floats-basics" moved from test/c to test/regressionGravatar xleroy2013-04-20
* Interp.ml: support printf of long longGravatar xleroy2013-04-20
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:Gravatar xleroy2013-04-20
* Updated issues with coqchk. See PR#3026 on the Coq bug tracker.Gravatar xleroy2013-04-14
* List.iteri not in OCaml < 4.00, better not use it.Gravatar xleroy2013-04-08
* UpdatedGravatar xleroy2013-03-26
* Error when calling un-prototyped function.Gravatar xleroy2013-03-25
* Better locations for error messages relative to type specifiers.Gravatar xleroy2013-03-25
* Watch out for behaviors exponential in the nesting of struct/union types. Gravatar xleroy2013-03-23
* RTLtyping: now performed entirely in Coq, no need for an external Caml oracle...Gravatar xleroy2013-03-22
* Update clightgen to changes in Camlcoq and in AST.Gravatar xleroy2013-03-20
* Diab asm syntax issueGravatar xleroy2013-03-20
* For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a ...Gravatar xleroy2013-03-18