Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Wrong handling of block-local function declarations (again) | Xavier Leroy | 2015-01-01 | 1 | -12/+7 |
| | | | | | Reapply commit c3b615f875ed2cf8418453c79c4621d2dc61b0a0 which was overwritten by 2d32afc5daf16c75d1a34f2716c34ae2e1efcce4 | ||||
* | Revised type compatibility check w.r.t. handling of attributes. | Xavier Leroy | 2015-01-01 | 4 | -49/+93 |
| | | | | | | | We now distinguish 3 modes (instead of 2 previously) for attributes: 1- strict compatibility, 2- ignore top-level attrs, 3- ignore all attrs recursively. In strict mode, const/volatile/restrict attributes must be identical, but nonstandard attributes may vary. Also: ignore top-level attrs when comparing function argument types, like GCC/Clang do. Net result is fewer warnings and type-checking that is closer to GCC/Clang. | ||||
* | PR#12: regression introduced in commit 2d32afc | Xavier Leroy | 2014-12-30 | 1 | -2/+0 |
| | |||||
* | PR#6: fix handling of wchar_t and assignments from wide string literals. | Xavier Leroy | 2014-12-30 | 5 | -9/+31 |
| | | | | | | | | | | - cparser/Machine indicates whether wchar_t is signed or not (it is signed int in Linux and BSD, but unsigned short in Win32) - The type of a wide string literal is "wchar_t *" if the typedef "wchar_t" exists in the environment (e.g. after #include <stddef.h>). Only if wchar_t is not defined do we use the default from Machine. - Permit initialization of any integer array from a wide string literal, not just an array of wchar_t. | ||||
* | PR#11: support sizeof(struct {...}) and _Alignof(struct {...}) | Xavier Leroy | 2014-12-30 | 1 | -25/+38 |
| | | | | This is a partial fix because other cases of struct definitions within type-names are still not handled, e.g. (struct { ... } *) <expr>. However, error reporting was improved for these cases. | ||||
* | Improve printing of errors. | Xavier Leroy | 2014-12-30 | 1 | -3/+11 |
| | |||||
* | PR#10 continued: disambiguate record to avoid OCaml warning | Xavier Leroy | 2014-12-30 | 1 | -1/+1 |
| | |||||
* | PR#10: composite definitions must be maintained in the environment. | Xavier Leroy | 2014-12-30 | 1 | -6/+15 |
| | |||||
* | cparser/Parser.v is generated. | Xavier Leroy | 2014-12-30 | 1 | -0/+1 |
| | |||||
* | Recognize more of GCC's alternate keywords (e.g. "__signed"). | Xavier Leroy | 2014-12-29 | 1 | -21/+24 |
| | | | | | Based on the source of GCC 4.9.2. Plus: reordered keywords in alphabetic order to facilitate comparison. | ||||
* | Support "asm volatile" (closes: PR#5). | Xavier Leroy | 2014-12-29 | 2 | -1/+3 |
| | | | | The CompCert back-end already treats "asm" inserts as "volatile" in GCC's sense (performing unpredictable side-effects), so no change is required outside of the parser. | ||||
* | 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 |
| | | | | Assorted updates to configure and Makefile. | ||||
* | Merge pull request #3 from AbsInt/pure-makefiles | Xavier Leroy | 2014-12-18 | 8 | -85/+371 |
|\ | | | | | Merge of the pure-makefiles branch, which uses Makefiles instead of ocamlbuild to build the Caml code. | ||||
| * | 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 ↵ | Xavier Leroy | 2014-12-17 | 6 | -39/+71 |
| | | | | | | | | common. | ||||
* | | Use cp instead of symbolic links for executables. | Xavier Leroy | 2014-12-17 | 1 | -15/+8 |
| | | | | | | | | Now that we search for compcert.ini from Sys.executable, symbolic links cause compcert.ini not to be found. | ||||
* | | 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 |
| | | | | | | | | | | | | | | | | | | - Prefix symbols with _ - Print indirect symbol definitions - Suppress __asm() macros in system header files | ||||
| * | | Prevent constant propagation on Oindirectsymbol addresses. | Xavier Leroy | 2014-12-11 | 1 | -2/+11 |
| | | | | | | | | | | | | | | | (Otherwise they are turned into Oaddrsymbol or global addressing modes, causing linking issues on MacOS X.) | ||||
| * | | 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 ↵ | Xavier Leroy | 2014-12-17 | 1 | -1/+1 |
|/ / | | | | | | | passes the reference interpreter. | ||||
* | | Removed more unused variables. | Bernhard Schommer | 2014-12-04 | 1 | -1/+0 |
| | | |||||
* | | Removed unused variable and changed the search for the installation ↵ | Bernhard Schommer | 2014-12-04 | 2 | -6/+1 |
| | | | | | | | | directory. Use Sys.executable_name instead of Sys.argv.(0). | ||||
* | | 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 |
| | | | | | | | | 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 |
| |