aboutsummaryrefslogtreecommitdiffstats
path: root/Changelog
Commit message (Collapse)AuthorAgeFilesLines
...
* Update Changelog for release 2.6.Xavier Leroy2015-12-191-0/+49
|
* More updates for release 2.5.Xavier Leroy2015-06-111-4/+5
|
* Update for release 2.5.Xavier Leroy2015-06-111-6/+11
|
* Update Changelog for release 2.5.Xavier Leroy2015-06-051-4/+79
|
* No longer include a pre-generated Parser.v in the distribution.Xavier Leroy2014-12-181-0/+5
| | | | Assorted updates to configure and Makefile.
* cchecklink: added option "-files-from" to read .sdump file namesXavier Leroy2014-11-151-1/+2
| | | | from a file or from standard input.
* Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0.Xavier Leroy2014-10-091-0/+1
|
* Error instead of warning on illegal escape sequences.Xavier Leroy2014-09-211-0/+4
| | | | | | | | The previous behavior for illegal escape sequences (e.g. '\%') in character and string literals was to emit an error, then treat "\x" as "x". As reported by a user, this is dangerous, because the warning can go unnoticed, and other compilers can treat "\x" as "\\x" (backslash followed by 'x'). Better to error out.
* Update changelog and version for 2.4xleroy2014-09-171-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2624 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cold feet: suppress builtins for load with reservation/store conditional, ↵xleroy2014-08-281-2/+0
| | | | | | use case is unclear. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updatexleroy2014-08-281-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2621 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for 2.4xleroy2014-08-271-23/+37
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2620 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Rename __builtin_cntlz to __builtin_clz.xleroy2014-08-271-0/+6
| | | | | | | IA32: add __builtin_clz, __builtin_ctz. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support C99 compound literals (by expansion in Unblock pass).xleroy2014-08-211-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-0/+6
| | | | | | | | | | | | | (in CompCert C to Cminor, included) - Translation of "switch" to decision trees or jumptables made generic over the sizes of integers and moved to the Cminor->CminorSel pass instead of CminorSel->RTL as before. - CminorSel: add "exitexpr" to support the above. - ValueDomain: more precise analysis of comparisons against an integer literal. E.g. "x >=u 0" is always true. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-281-0/+4
| | | | | | | | | | pseudo-instructions so that it does not need to be re-done in cchecklink. cchecklink: updated accordingly. testsuite: compile with -sdump and run cchecklink if supported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated Changelogxleroy2014-07-281-0/+28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2552 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Document commit r2507.xleroy2014-06-051-0/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2508 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Re-added support for "__func__" identifier as per ISO C99.xleroy2014-05-151-2/+8
| | | | | | | | - Support for empty structs and unions - Better handling of "extern" and "extern inline" function definitions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2493 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed regression on initializers of the form T x[N] = "literal";xleroy2014-05-081-0/+9
| | | | | | | where T is a typedef for a character type. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2488 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for release 2.3.xleroy2014-05-051-0/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2482 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fused multiply-add for IA32.xleroy2014-05-051-4/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2481 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM: honor common variables.xleroy2014-05-021-1/+3
| | | | | | | Changelog: update. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2475 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-0/+10
| | | | | | | (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update with post-2.2 changesxleroy2014-04-231-0/+36
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2460 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates for release 2.2xleroy2014-02-211-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2415 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-0/+2
| | | | | | | | Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for 2.2, continuedxleroy2014-02-161-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for release 2.2.xleroy2014-02-151-13/+74
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2408 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Recognize .i and .p source files as C sources not to be preprocessed.xleroy2014-02-051-1/+2
| | | | | | | Add CompCert version number and command line as comments in generated asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2407 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-1/+3
| | | | | | | - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More tolerance for functions declared without a prototypexleroy2013-12-281-1/+3
| | | | | | | | (option -funprototyped, on by default). Error if call to vararg function and -fvararg-calls is off. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2389 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-0/+1
| | | | | | | | | | | | | | - C function types and Cminor signatures annotated by calling conventions. esp. vararg / not vararg - Cshmgen: generate correct code for function call where there are more arguments than listed in the function prototype. This is still undefined behavior according to the formal semantics, but correct code is generated. - C2C, */PrintAsm.ml: remove "printf$iif" hack. - powerpc/, checklink/: don't generate stubs for variadic functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised parsing of command-line options, more GCC-like.xleroy2013-12-211-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support "default" cases in the middle of a "switch", not just at the end.xleroy2013-12-211-1/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Recognize __builtin_fabs as an operator, not just a builtin,xleroy2013-11-061-0/+10
| | | | | | | | | enabling more aggressive optimizations. - Less aggressive CSE for EF_builtin builtins, causes problems for __builtin_write{16,32}_reversed. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2363 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MAJ release 2.1v2.1xleroy2013-10-281-10/+25
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2355 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "alignas" branch.xleroy2013-10-051-0/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Small improvements in compilation times for the register allocation pass.xleroy2013-09-201-0/+2
| | | | | | | Maps.v: add a PTree.fold1 operation that doesn't maintain the key. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2329 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms xleroy2013-09-141-0/+5
| | | | | | | | | are necessary, only two parameters (default_pl and choose_binop_pl). SelectDiv: optimize FP division by a power of 2. ConstpropOp: optimize 2.0 * x and x * 2.0 into x + x. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2326 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Change interface of Kildall solvers to avoid precomputing the map pc -> list ↵xleroy2013-08-121-1/+1
| | | | | | of successors. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2305 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of Flocq version 2.2.0.xleroy2013-08-021-0/+2
| | | | | | | More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+2
| | | | | | | multiply-high and shifts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-0/+8
| | | | | | | | casts int64 -> float64 -> float32. The latter causes double rounding errors. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2290 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Version 2.00 -> version 2.0v2.0xleroy2013-06-211-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates in preparation for release 2.00xleroy2013-06-191-5/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for release 2.00xleroy2013-06-161-3/+60
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2277 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Watch out for behaviors exponential in the nesting of struct/union types. xleroy2013-03-231-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More aggressive CSE across Ibuiltin.xleroy2013-03-171-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2152 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Assorted changes to reduce stack and heap requirements when compiling very ↵xleroy2013-03-161-0/+8
| | | | | | big functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-19 21:23:52 +0000