aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | 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
| | |\ \ | | |/ / | |/| |
| | * | Use OCaml's .opt compilers when available.Xavier Leroy2014-12-173-32/+82
| | | | | | | | | | | | | | | | Cleanups in configure.
| | * | 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
| | | | | | | | | | | | | | | | Avoids warnings with 4.02.
| | * | Replace ocamlbuild by a second-stage makefile to compile the OCaml code and ↵Xavier Leroy2014-11-225-59/+296
| | | | | | | | | | | | | | | | | | | | | | | | produce the executables. configure: add check for GNU make.
* | | | Added dummy printing function for entries.Bernhard Schommer2014-12-181-1/+4
| | | |
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-1710-58/+88
|\| | | | | | | | | | | | | | | | | | | Conflicts: powerpc/PrintAsm.ml
| * | | 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
| | | | |
| * | | | Prototype the pointer so that the program has well defined semantics and ↵Xavier Leroy2014-12-171-1/+1
| | | | | | | | | | | | | | | | | | | | passes the reference interpreter.
* | | | | Added more printing code.Bernhard Schommer2014-12-151-3/+8
| | | | |
* | | | | Started implementation of printing the dwarf entries.Bernhard Schommer2014-12-153-11/+31
| | | | |
* | | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-114-17/+28
|\ \ \ \ \ | | |/ / / | |/| | |
| * | | | 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
| |/ / /
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-041-1/+0
|\| | |
| * | | Removed more unused variables.Bernhard Schommer2014-12-041-1/+0
| | | |
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-042-6/+1
|\| | |
| * | | 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 d1line and d1file to d2line and d2file and prologue and epilogue ↵Bernhard Schommer2014-12-045-9/+79
| | | | | | | | | | | | | | | | printing for printing the line directives without forcing the assembler to generate debug information.
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-021-14/+7
|\| | |
| * | | Changed the comparison of jumptables.Bernhard Schommer2014-12-011-14/+7
| | | |
* | | | Renamed the printer module for the Abbreviations and deactivated adding the ↵Bernhard Schommer2014-12-023-47/+11
| | | | | | | | | | | | | | | | -g option to the assembler.
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-11-2750-684/+2264
|\| | |
| * | | 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.
| * / Use gettimeofday() instead of obsolete ftime().Xavier Leroy2014-11-242-11/+19
| |/ | | | | | | (Patch by Daniel Dickman.)
* | Merge branch 'master' into dwarfBernhard Schommer2014-11-191-1/+1
|\|
| * Analysis of jump tables was using the wrong size.Xavier Leroy2014-11-171-1/+1
| |
generated by cgit (git 2.34.1) at 2024-07-20 18:22:12 +0000