aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into pure-makefilesXavier Leroy2014-12-1759-763/+2379
|\
| * Clean up support for common symbols. Uninitialized "const" symbols can be co...Xavier Leroy2014-12-176-39/+71
| * Use cp instead of symbolic links for executables.Xavier Leroy2014-12-171-15/+8
| * Merge branch 'master' of https://github.com/AbsInt/CompCertXavier Leroy2014-12-175-19/+35
| |\
| | * Stdlib path is ignored when the configuration has_runtime_lib is set to false.Bernhard Schommer2014-12-151-2/+7
| | * Update the IA32/MacOS X port.Xavier Leroy2014-12-112-5/+7
| | * Prevent constant propagation on Oindirectsymbol addresses.Xavier Leroy2014-12-111-2/+11
| | * Preserve single quotes (e.g. in CPREPRO) when generating compcert.iniXavier Leroy2014-12-111-10/+10
| * | Prototype the pointer so that the program has well defined semantics and pass...Xavier Leroy2014-12-171-1/+1
| |/
| * Removed more unused variables.Bernhard Schommer2014-12-041-1/+0
| * Removed unused variable and changed the search for the installation directory...Bernhard Schommer2014-12-042-6/+1
| * Changed the comparison of jumptables.Bernhard Schommer2014-12-011-14/+7
| * Wrong handling of block-local function declarations (in Elab.ml).Xavier Leroy2014-11-264-13/+31
| * Use Bitstring.is_zeroes_bitstring from bitstring 2.0.4.Xavier Leroy GALLIUM2014-11-251-0/+8
| * Merge pull request #2 from AbsInt/public-globalsXavier Leroy2014-11-2543-660/+2206
| |\
| | * Update the ARM port.Xavier Leroy2014-11-242-50/+38
| | * Update PowerPC port.Xavier Leroy2014-11-242-21/+51
| | * Verification of the Unusedglob pass (removal of unreferenced static global de...Xavier Leroy2014-11-2412-264/+1458
| | * Add Genv.public_symbol operation.Xavier Leroy2014-11-2424-263/+562
| | * Record public global definitions via field "prog_public" in AST.program.Xavier Leroy2014-11-247-63/+98
| |/
| * Use gettimeofday() instead of obsolete ftime().Xavier Leroy2014-11-242-11/+19
* | Use OCaml's .opt compilers when available.Xavier Leroy2014-12-173-32/+82
* | Remove ocamlbuild configuration files, no longer used.Xavier Leroy2014-11-222-23/+0
* | Use String.map instead of reimplementing it ourselves.Xavier Leroy2014-11-221-5/+18
* | Replace ocamlbuild by a second-stage makefile to compile the OCaml code and p...Xavier Leroy2014-11-225-59/+296
|/
* Analysis of jump tables was using the wrong size.Xavier Leroy2014-11-171-1/+1
* Add flags to control individual optimization passes + flag -O0 for turning th...Xavier Leroy2014-11-167-46/+128
* Revised parsing of command-line arguments (in preparation for adding more).Xavier Leroy2014-11-163-118/+250
* build_from_parsed: simplified code + correctness proof.Xavier Leroy2014-11-151-15/+86
* cchecklink: added option "-files-from" to read .sdump file namesXavier Leroy2014-11-152-4/+29
* Tune behavior wrt warnings:Xavier Leroy2014-10-242-2/+3
* Deactivated the warning for deprecated features for compilation of cchecklink...Bernhard Schommer2014-10-201-0/+1
* Removed duplicated open.Bernhard Schommer2014-10-171-1/+0
* Revised translation of '&&' and '||' to Clight.Xavier Leroy2014-10-1311-124/+109
* Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0.Xavier Leroy2014-10-093-1/+3
* Merge pull request #1 from jhjourdan/masterXavier Leroy2014-10-0921-942/+6030
|\
| * Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-0721-942/+6030
* | Refactored the code of ia32/PrintAsm.ml by moving the functions depending on ...Bernhard Schommer2014-10-081-138/+220
* | Refactored the code of powerpc/PrintAsm.ml by moving the function depending o...Bernhard Schommer2014-10-081-200/+236
|/
* Refactored the code of arm/PrintAsm.ml in order to allow the parametrization ...Bernhard Schommer2014-10-061-44/+86
* Removed environment variable for the stdlib_path and added a new variable for...Bernhard Schommer2014-10-063-20/+20
* Change the way the tools like the linker, assembler, etc. are specified by in...Bernhard Schommer2014-09-304-22/+113
* Moved the timing facility to a seperate file.Bernhard Schommer2014-09-295-54/+68
* Refactoring in the printing of FP numbers.Xavier Leroy2014-09-241-8/+2
* Add theorem "elements_remove".Xavier Leroy2014-09-241-167/+178
* Upgrade clightgen with the new features of CompCert 2.4 (single floats, etc).Xavier Leroy2014-09-241-7/+20
* GCCism: accept __volatile and __volatile__Xavier Leroy2014-09-211-0/+2
* Add .gitignore files.Xavier Leroy2014-09-216-0/+63
* Error instead of warning on illegal escape sequences.Xavier Leroy2014-09-212-1/+5
* Trim blank linesv2.4xleroy2014-09-171-2/+0
generated by cgit (git 2.34.1) at 2024-07-03 18:24:46 +0000