Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| | * | | 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 | |
| | |/ | |/| | ||||||
| * | | 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.) | |||||
* | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-11-19 | 1 | -1/+1 | |
|\| | ||||||
| * | Analysis of jump tables was using the wrong size. | Xavier Leroy | 2014-11-17 | 1 | -1/+1 | |
| | | ||||||
* | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-11-17 | 12 | -179/+489 | |
|\| | ||||||
| * | 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. | |||||
* | | Removed compile error and added dummy function for the printing of entries. | Bernhard Schommer | 2014-11-17 | 3 | -8/+12 | |
| | | ||||||
* | | More functionality for the Printer. | Bernhard Schommer | 2014-11-14 | 1 | -1/+4 | |
| | | ||||||
* | | Moved abbreviation printer into a seperate file. The printer should also ↵ | Bernhard Schommer | 2014-11-12 | 3 | -325/+394 | |
| | | | | | | | | print the debug info. | |||||
* | | Added functions for printing of the abbreviations. | Bernhard Schommer | 2014-11-11 | 3 | -3/+41 | |
| | | ||||||
* | | Generalised functionality for the printing of the abbreviations. | Bernhard Schommer | 2014-11-11 | 2 | -235/+307 | |
| | | ||||||
* | | Added more functions to print the abbreviations. | Bernhard Schommer | 2014-11-06 | 2 | -99/+167 | |
| | | ||||||
* | | More functions for printing the abbreviations. | Bernhard Schommer | 2014-10-31 | 2 | -77/+141 | |
| | | ||||||
* | | Reverted changes to C2C since the information needed should be stored ↵ | Bernhard Schommer | 2014-10-30 | 1 | -16/+4 | |
| | | | | | | | | already earlier. | |||||
* | | Started implementing functions to compute the abbreviations for the diab ↵ | Bernhard Schommer | 2014-10-29 | 2 | -13/+87 | |
| | | | | | | | | compiler. | |||||
* | | Refactored the printing functions a little bit more by moving the system ↵ | Bernhard Schommer | 2014-10-28 | 4 | -328/+397 | |
| | | | | | | | | dependent parts into other modules and some of the functions into a util file. | |||||
* | | Added the type information to the global information stored for each atom. | Bernhard Schommer | 2014-10-27 | 2 | -5/+20 | |
| | |