Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | | | 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 | |
| | | | | | | | | The original code is less efficient and not tail recursive. | |||||
* | | Merge pull request #2 from AbsInt/public-globals | Xavier Leroy | 2014-11-25 | 43 | -660/+2206 | |
|\ \ | | | | | | | Public globals | |||||
| * | | 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 ↵ | Xavier Leroy | 2014-11-24 | 12 | -264/+1458 | |
| | | | | | | | | | | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating. | |||||
| * | | Add Genv.public_symbol operation. | Xavier Leroy | 2014-11-24 | 24 | -263/+562 | |
| | | | | | | | | | | | | | | | Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating. | |||||
| * | | Record public global definitions via field "prog_public" in AST.program. | Xavier Leroy | 2014-11-24 | 7 | -63/+98 | |
|/ / | | | | | | | For the moment, this field is ignored. | |||||
* | | Use gettimeofday() instead of obsolete ftime(). | Xavier Leroy | 2014-11-24 | 2 | -11/+19 | |
| | | | | | | | | (Patch by Daniel Dickman.) | |||||
| * | Use OCaml's .opt compilers when available. | Xavier Leroy | 2014-12-17 | 3 | -32/+82 | |
| | | | | | | | | Cleanups in configure. | |||||
| * | 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 | |
| | | | | | | | | Avoids warnings with 4.02. | |||||
| * | Replace ocamlbuild by a second-stage makefile to compile the OCaml code and ↵ | Xavier Leroy | 2014-11-22 | 5 | -59/+296 | |
|/ | | | | | | produce the executables. configure: add check for GNU make. | |||||
* | 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 ↵ | Xavier Leroy | 2014-11-16 | 7 | -46/+128 | |
| | | | | them off. | |||||
* | Revised parsing of command-line arguments (in preparation for adding more). | Xavier Leroy | 2014-11-16 | 3 | -118/+250 | |
| | | | | | | Honor "ccomp -E foo.h" for GCC compatibility. Accept .o.ext files as object files for GCC compatibility. Fixed and improved handling of Cminor source files. | |||||
* | 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 | |
| | | | | from a file or from standard input. | |||||
* | Tune behavior wrt warnings: | Xavier Leroy | 2014-10-24 | 2 | -2/+3 | |
| | | | | | | - cchecklink was compiled with -warn-error, which is bad for production code - silence warning 3 (deprecated functions) - silence warning 20 (unused function argument) for Coq-extracted files. | |||||
* | Deactivated the warning for deprecated features for compilation of ↵ | Bernhard Schommer | 2014-10-20 | 1 | -0/+1 | |
| | | | | cchecklink since it breaks the build with newer ocaml versions. | |||||
* | 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 | |
| | | | | | | | | | | | The previous translation (in SimplExpr) produced references to the same temporary variable with two different types (bool and int), which is not nice if we want to typecheck the generated Clight. The new translation avoids this and also gets rid of the double cast to bool then to int. The trick is to change Eparen (in CompCert C expressions) to take two types: the type to which the argument must be converted, and the type with which the resulting expression is seen. | |||||
* | 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 | |||||
| * | 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 | |
| | | | | | | | | the target system in a seperate module. | |||||
* | | Refactored the code of powerpc/PrintAsm.ml by moving the function depending ↵ | Bernhard Schommer | 2014-10-08 | 1 | -200/+236 | |
|/ | | | | on the target system in a seperate module. | |||||
* | Refactored the code of arm/PrintAsm.ml in order to allow the parametrization ↵ | Bernhard Schommer | 2014-10-06 | 1 | -44/+86 | |
| | | | | of the printing code over the configuration-dependent bits. | |||||
* | Removed environment variable for the stdlib_path and added a new variable ↵ | Bernhard Schommer | 2014-10-06 | 3 | -20/+20 | |
| | | | | for the configuration file. | |||||
* | Change the way the tools like the linker, assembler, etc. are specified by ↵ | Bernhard Schommer | 2014-09-30 | 4 | -22/+113 | |
| | | | | including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start. | |||||
* | 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 | |
| | ||||||
* | Add theorem "elements_remove". | Xavier Leroy | 2014-09-24 | 1 | -167/+178 | |
| | | | | | Use "elements_remove" to simplify the proof of "cardinal_remove". Simplify some of the proofs over function "xelements". | |||||
* | Upgrade clightgen with the new features of CompCert 2.4 (single floats, etc). | Xavier Leroy | 2014-09-24 | 1 | -7/+20 | |
| | ||||||
* | GCCism: accept __volatile and __volatile__ | Xavier Leroy | 2014-09-21 | 1 | -0/+2 | |
| | | | | | These alternate keywords for "volatile" are used in some header files in the wild. | |||||
* | Add .gitignore files. | Xavier Leroy | 2014-09-21 | 6 | -0/+63 | |
| | ||||||
* | Error instead of warning on illegal escape sequences. | Xavier Leroy | 2014-09-21 | 2 | -1/+5 | |
| | | | | | | | | 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. | |||||
* | Trim blank linesv2.4 | xleroy | 2014-09-17 | 1 | -2/+0 | |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2625 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
* | Update changelog and version for 2.4 | xleroy | 2014-09-17 | 2 | -3/+4 | |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2624 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
* | Tolerance in parsing of 'section' pragma | xleroy | 2014-09-17 | 1 | -0/+3 | |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2623 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
* | Cold feet: suppress builtins for load with reservation/store conditional, ↵ | xleroy | 2014-08-28 | 5 | -47/+2 | |
| | | | | | | use case is unclear. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
* | Update | xleroy | 2014-08-28 | 1 | -1/+2 | |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2621 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
* | Update for 2.4 | xleroy | 2014-08-27 | 1 | -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. | xleroy | 2014-08-27 | 11 | -6/+25 | |
| | | | | | | | IA32: add __builtin_clz, __builtin_ctz. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
* | More efficient implementations of map, fold, etc. | xleroy | 2014-08-27 | 1 | -164/+109 | |
| | | | | | | | (Contributed by Vincent Laporte.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2618 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
* | More careful detection of inlined builtins. Produces better error messages ↵ | xleroy | 2014-08-25 | 1 | -0/+1 | |
| | | | | | | if an unsupported __builtin_xxx function is used by mistake. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2617 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
* | Use VFD regs to implement 64-bit mem-mem copies in builtin_memcpy_false. | xleroy | 2014-08-21 | 3 | -5/+10 | |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
* | Support C99 compound literals (by expansion in Unblock pass). | xleroy | 2014-08-21 | 16 | -454/+801 | |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
* | Follow-up to commit 2613 | xleroy | 2014-08-20 | 1 | -0/+2 | |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2614 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
* | Add builtins for load with reservation and conditional store. | xleroy | 2014-08-20 | 5 | -1/+39 | |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2613 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e |