Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-01-12 | 34 | -61988/+914 |
|\ | | | | | | | | | Conflicts: powerpc/PrintAsm.ml | ||||
| * | In -g -S mode, annotate the generated asm file with the C source code in ↵ | Xavier Leroy | 2015-01-07 | 6 | -86/+243 |
| | | | | | | | | | | | | comments. Refactor printing of .loc debug directives in backend/PrintAnnot.ml | ||||
| * | PR#19: there is no reason to reject an empty "switch" statement. | Xavier Leroy | 2015-01-06 | 1 | -2/+0 |
| | | |||||
| * | PR#16: give option rules precedence over file pattern rules. | Xavier Leroy | 2015-01-03 | 3 | -31/+38 |
| | | | | | | | | | | | | Plus: simplify handling of -help and --help. Plus: error on unrecognized "-xxx" options so that "-foo.c" is not treated as a source file. | ||||
| * | PR#14: recognize ".so" arguments as files to pass to the linker. | Xavier Leroy | 2015-01-02 | 1 | -1/+2 |
| | | |||||
| * | PR#15: vararg functions are not eligible for inlining. | Xavier Leroy | 2015-01-02 | 1 | -1/+1 |
| | | |||||
| * | Translation of wide string literals. | Xavier Leroy | 2015-01-01 | 1 | -6/+57 |
| | | | | | | | | | | | | | | Closes PR#13. Also: give string literals type unsigned char [] or signed char [] depending on the machine configuration. (Instead of unsigned char [] before.) | ||||
| * | 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 |
| | |\ | | |/ | |/| | |||||
| | * | 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. | ||||
* | | | Added dummy printing function for entries. | Bernhard Schommer | 2014-12-18 | 1 | -1/+4 |
| | | | |||||
* | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-12-17 | 10 | -58/+88 |
|\| | | | | | | | | | | | | | | Conflicts: powerpc/PrintAsm.ml | ||||
| * | | 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 |
| | | | | |||||
| * | | | Prototype the pointer so that the program has well defined semantics and ↵ | Xavier Leroy | 2014-12-17 | 1 | -1/+1 |
| | | | | | | | | | | | | | | | | passes the reference interpreter. | ||||
* | | | | Added more printing code. | Bernhard Schommer | 2014-12-15 | 1 | -3/+8 |
| | | | | |||||
* | | | | Started implementation of printing the dwarf entries. | Bernhard Schommer | 2014-12-15 | 3 | -11/+31 |
| | | | | |||||
* | | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-12-11 | 4 | -17/+28 |
|\ \ \ \ | | |/ / | |/| | | |||||
| * | | | 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 |
| |/ / | |||||
* | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-12-04 | 1 | -1/+0 |
|\| | | |||||
| * | | Removed more unused variables. | Bernhard Schommer | 2014-12-04 | 1 | -1/+0 |
| | | | |||||
* | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-12-04 | 2 | -6/+1 |
|\| | | |||||
| * | | 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 d1line and d1file to d2line and d2file and prologue and epilogue ↵ | Bernhard Schommer | 2014-12-04 | 5 | -9/+79 |
| | | | | | | | | | | | | printing for printing the line directives without forcing the assembler to generate debug information. | ||||
* | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-12-02 | 1 | -14/+7 |
|\| | | |||||
| * | | Changed the comparison of jumptables. | Bernhard Schommer | 2014-12-01 | 1 | -14/+7 |
| | | | |||||
* | | | Renamed the printer module for the Abbreviations and deactivated adding the ↵ | Bernhard Schommer | 2014-12-02 | 3 | -47/+11 |
| | | | | | | | | | | | | -g option to the assembler. | ||||
* | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-11-27 | 50 | -684/+2264 |
|\| | | |||||
| * | | Wrong handling of block-local function declarations (in Elab.ml). | Xavier Leroy | 2014-11-26 | 4 | -13/+31 |
| | | |