aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch containing changes for windows compile.Bernhard Schommer2015-01-203-8/+15
|\
| * Renamed LIB into VLIB to avoid clashes with environment variables.Bernhard Schommer2015-01-201-2/+2
| |
| * Replaced 8 spaces by tabs.Bernhard Schommer2015-01-161-1/+1
| |
| * Added new target to just remove the cm[iox] files and the build executables.Bernhard Schommer2015-01-161-0/+4
| |
| * Added missing $ for build_checklinkBernhard Schommer2015-01-151-2/+2
| |
| * Added variable to the Makefile to specify additional linker commands and ↵Bernhard Schommer2015-01-153-6/+9
| | | | | | | | changed the configure script to deactivated the checklink build if needed.
* | Protect against redefinition of the __i64_xxx helper library functions.Xavier Leroy2015-01-206-251/+306
| | | | | | | | | | | | | | | | | | | | This is achieved by declaring these functions in C2C.ml, then re-checking their declarations in the global environment during the Selection pass. In passing, the "hf" parameter for SelectLong functions was removed and replaced by fixed identifiers corresponding to the actual names of the helper functions.
* | Follow-up to [5aecefe]: be conservative also in the case of a "common" ↵Xavier Leroy2015-01-201-6/+21
|/ | | | global const variable.
* More prudent analysis of uninitialized const global variables.Xavier Leroy2015-01-091-3/+6
| | | | | | | In the presence of separate compilation and linking, an uninitialized const global variable may be initialized elsewhere with a pointer value, falsifying the points-to analysis. Report and fix by Chung-Kil Hur and Jeehoon Kang.
* In -g -S mode, annotate the generated asm file with the C source code in ↵Xavier Leroy2015-01-076-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 Leroy2015-01-061-2/+0
|
* PR#16: give option rules precedence over file pattern rules.Xavier Leroy2015-01-033-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 Leroy2015-01-021-1/+2
|
* PR#15: vararg functions are not eligible for inlining.Xavier Leroy2015-01-021-1/+1
|
* Translation of wide string literals.Xavier Leroy2015-01-011-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 Leroy2015-01-011-12/+7
| | | | | Reapply commit c3b615f875ed2cf8418453c79c4621d2dc61b0a0 which was overwritten by 2d32afc5daf16c75d1a34f2716c34ae2e1efcce4
* Revised type compatibility check w.r.t. handling of attributes.Xavier Leroy2015-01-014-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 2d32afcXavier Leroy2014-12-301-2/+0
|
* PR#6: fix handling of wchar_t and assignments from wide string literals.Xavier Leroy2014-12-305-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 Leroy2014-12-301-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 Leroy2014-12-301-3/+11
|
* PR#10 continued: disambiguate record to avoid OCaml warningXavier Leroy2014-12-301-1/+1
|
* PR#10: composite definitions must be maintained in the environment.Xavier Leroy2014-12-301-6/+15
|
* cparser/Parser.v is generated.Xavier Leroy2014-12-301-0/+1
|
* Recognize more of GCC's alternate keywords (e.g. "__signed").Xavier Leroy2014-12-291-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 Leroy2014-12-292-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 Leroy2014-12-181-1/+1
|
* No longer include a pre-generated Parser.v in the distribution.Xavier Leroy2014-12-184-61679/+15
| | | | Assorted updates to configure and Makefile.
* Merge pull request #3 from AbsInt/pure-makefilesXavier Leroy2014-12-188-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.extrXavier Leroy2014-12-172-5/+6
| |
| * Merge branch 'master' into pure-makefilesXavier Leroy2014-12-1759-763/+2379
| |\ | |/ |/|
* | Clean up support for common symbols. Uninitialized "const" symbols can be ↵Xavier Leroy2014-12-176-39/+71
| | | | | | | | common.
* | Use cp instead of symbolic links for executables.Xavier Leroy2014-12-171-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/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
| | | | | | | | | | | | | | | | | | - Prefix symbols with _ - Print indirect symbol definitions - Suppress __asm() macros in system header files
| * | Prevent constant propagation on Oindirectsymbol addresses.Xavier Leroy2014-12-111-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.iniXavier Leroy2014-12-111-10/+10
| | |
* | | Prototype the pointer so that the program has well defined semantics and ↵Xavier Leroy2014-12-171-1/+1
|/ / | | | | | | passes the reference interpreter.
* | Removed more unused variables.Bernhard Schommer2014-12-041-1/+0
| |
* | Removed unused variable and changed the search for the installation ↵Bernhard Schommer2014-12-042-6/+1
| | | | | | | | directory. Use Sys.executable_name instead of Sys.argv.(0).
* | 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
| | | | | | | | The original code is less efficient and not tail recursive.
* | Merge pull request #2 from AbsInt/public-globalsXavier Leroy2014-11-2543-660/+2206
|\ \ | | | | | | Public globals
| * | 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 ↵Xavier Leroy2014-11-2412-264/+1458
| | | | | | | | | | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
| * | Add Genv.public_symbol operation.Xavier Leroy2014-11-2424-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 Leroy2014-11-247-63/+98
|/ / | | | | | | For the moment, this field is ignored.
generated by cgit (git 2.34.1) at 2024-07-03 08:42:23 +0000