Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | | | | | | | | | | | | | | | Recognize more of GCC's alternate keywords (e.g. "__signed"). | Xavier Leroy | 2014-12-29 | 1 | -21/+24 | |
* | | | | | | | | | | | | | | | Support "asm volatile" (closes: PR#5). | Xavier Leroy | 2014-12-29 | 2 | -1/+3 | |
| |/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | ||||||
* | | | | | | | | | | | | | | One more cleanup in configure. | Xavier Leroy | 2014-12-18 | 1 | -1/+1 | |
* | | | | | | | | | | | | | | No longer include a pre-generated Parser.v in the distribution. | Xavier Leroy | 2014-12-18 | 4 | -61679/+15 | |
* | | | | | | | | | | | | | | Merge pull request #3 from AbsInt/pure-makefiles | Xavier Leroy | 2014-12-18 | 8 | -85/+371 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | ||||||
| * | | | | | | | | | | | | | Minor bug fixes in configure and Makefile.extr | Xavier Leroy | 2014-12-17 | 2 | -5/+6 | |
| * | | | | | | | | | | | | | Merge branch 'master' into pure-makefiles | Xavier Leroy | 2014-12-17 | 59 | -763/+2379 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | ||||||
* | | | | | | | | | | | | | | Clean up support for common symbols. Uninitialized "const" symbols can be co... | Xavier Leroy | 2014-12-17 | 6 | -39/+71 | |
* | | | | | | | | | | | | | | Use cp instead of symbolic links for executables. | Xavier Leroy | 2014-12-17 | 1 | -15/+8 | |
* | | | | | | | | | | | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert | Xavier Leroy | 2014-12-17 | 5 | -19/+35 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||||
| * | | | | | | | | | | | | | | Stdlib path is ignored when the configuration has_runtime_lib is set to false. | Bernhard Schommer | 2014-12-15 | 1 | -2/+7 | |
| | |_|_|_|_|_|_|_|_|_|_|_|/ | |/| | | | | | | | | | | | | ||||||
| * | | | | | | | | | | | | | Update the IA32/MacOS X port. | Xavier Leroy | 2014-12-11 | 2 | -5/+7 | |
| * | | | | | | | | | | | | | Prevent constant propagation on Oindirectsymbol addresses. | Xavier Leroy | 2014-12-11 | 1 | -2/+11 | |
| * | | | | | | | | | | | | | Preserve single quotes (e.g. in CPREPRO) when generating compcert.ini | Xavier Leroy | 2014-12-11 | 1 | -10/+10 | |
| | |_|_|_|_|_|_|_|_|_|_|/ | |/| | | | | | | | | | | | ||||||
* / | | | | | | | | | | | | Prototype the pointer so that the program has well defined semantics and pass... | Xavier Leroy | 2014-12-17 | 1 | -1/+1 | |
|/ / / / / / / / / / / / | ||||||
* | | | | | | | | | | / | Removed more unused variables. | Bernhard Schommer | 2014-12-04 | 1 | -1/+0 | |
| |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | ||||||
* | | | | | | | | | | | Removed unused variable and changed the search for the installation directory... | Bernhard Schommer | 2014-12-04 | 2 | -6/+1 | |
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | ||||||
* | | | | | | | | | | Changed the comparison of jumptables. | Bernhard Schommer | 2014-12-01 | 1 | -14/+7 | |
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | ||||||
* | | | | | | | | | Wrong handling of block-local function declarations (in Elab.ml). | Xavier Leroy | 2014-11-26 | 4 | -13/+31 | |
| |/ / / / / / / |/| | | | | | | | ||||||
* | | | | | | | | Use Bitstring.is_zeroes_bitstring from bitstring 2.0.4. | Xavier Leroy GALLIUM | 2014-11-25 | 1 | -0/+8 | |
* | | | | | | | | Merge pull request #2 from AbsInt/public-globals | Xavier Leroy | 2014-11-25 | 43 | -660/+2206 | |
|\ \ \ \ \ \ \ \ | ||||||
| * | | | | | | | | Update the ARM port. | Xavier Leroy | 2014-11-24 | 2 | -50/+38 | |
| * | | | | | | | | Update PowerPC port. | Xavier Leroy | 2014-11-24 | 2 | -21/+51 | |
| * | | | | | | | | Verification of the Unusedglob pass (removal of unreferenced static global de... | Xavier Leroy | 2014-11-24 | 12 | -264/+1458 | |
| * | | | | | | | | Add Genv.public_symbol operation. | Xavier Leroy | 2014-11-24 | 24 | -263/+562 | |
| * | | | | | | | | Record public global definitions via field "prog_public" in AST.program. | Xavier Leroy | 2014-11-24 | 7 | -63/+98 | |
|/ / / / / / / / | ||||||
* | | | | | | / | Use gettimeofday() instead of obsolete ftime(). | Xavier Leroy | 2014-11-24 | 2 | -11/+19 | |
| |_|_|_|_|_|/ |/| | | | | | | ||||||
| * | | | | | | Use OCaml's .opt compilers when available. | Xavier Leroy | 2014-12-17 | 3 | -32/+82 | |
| * | | | | | | Remove ocamlbuild configuration files, no longer used. | Xavier Leroy | 2014-11-22 | 2 | -23/+0 | |
| * | | | | | | Use String.map instead of reimplementing it ourselves. | Xavier Leroy | 2014-11-22 | 1 | -5/+18 | |
| * | | | | | | Replace ocamlbuild by a second-stage makefile to compile the OCaml code and p... | Xavier Leroy | 2014-11-22 | 5 | -59/+296 | |
|/ / / / / / | ||||||
* | | | | / | Analysis of jump tables was using the wrong size. | Xavier Leroy | 2014-11-17 | 1 | -1/+1 | |
| |_|_|_|/ |/| | | | | ||||||
* | | | | | Add flags to control individual optimization passes + flag -O0 for turning th... | Xavier Leroy | 2014-11-16 | 7 | -46/+128 | |
* | | | | | Revised parsing of command-line arguments (in preparation for adding more). | Xavier Leroy | 2014-11-16 | 3 | -118/+250 | |
* | | | | | build_from_parsed: simplified code + correctness proof. | Xavier Leroy | 2014-11-15 | 1 | -15/+86 | |
* | | | | | cchecklink: added option "-files-from" to read .sdump file names | Xavier Leroy | 2014-11-15 | 2 | -4/+29 | |
| |_|_|/ |/| | | | ||||||
* | | | | Tune behavior wrt warnings: | Xavier Leroy | 2014-10-24 | 2 | -2/+3 | |
| |_|/ |/| | | ||||||
* | | | Deactivated the warning for deprecated features for compilation of cchecklink... | Bernhard Schommer | 2014-10-20 | 1 | -0/+1 | |
| |/ |/| | ||||||
* | | Removed duplicated open. | Bernhard Schommer | 2014-10-17 | 1 | -1/+0 | |
|/ | ||||||
* | Revised translation of '&&' and '||' to Clight. | Xavier Leroy | 2014-10-13 | 11 | -124/+109 | |
* | Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0. | Xavier Leroy | 2014-10-09 | 3 | -1/+3 | |
* | Merge pull request #1 from jhjourdan/master | Xavier Leroy | 2014-10-09 | 21 | -942/+6030 | |
|\ | ||||||
| * | Upgrade to flocq 2.4.0 | Jacques-Henri Jourdan | 2014-10-07 | 21 | -942/+6030 | |
* | | Refactored the code of ia32/PrintAsm.ml by moving the functions depending on ... | Bernhard Schommer | 2014-10-08 | 1 | -138/+220 | |
* | | Refactored the code of powerpc/PrintAsm.ml by moving the function depending o... | Bernhard Schommer | 2014-10-08 | 1 | -200/+236 | |
|/ | ||||||
* | Refactored the code of arm/PrintAsm.ml in order to allow the parametrization ... | Bernhard Schommer | 2014-10-06 | 1 | -44/+86 | |
* | Removed environment variable for the stdlib_path and added a new variable for... | Bernhard Schommer | 2014-10-06 | 3 | -20/+20 | |
* | Change the way the tools like the linker, assembler, etc. are specified by in... | Bernhard Schommer | 2014-09-30 | 4 | -22/+113 | |
* | Moved the timing facility to a seperate file. | Bernhard Schommer | 2014-09-29 | 5 | -54/+68 | |
* | Refactoring in the printing of FP numbers. | Xavier Leroy | 2014-09-24 | 1 | -8/+2 |