| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | 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 |
| | | | |||||
| * | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-10-27 | 2 | -2/+3 |
| |\| | |||||
| | * | 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. | ||||
| * | | Added more functionality to DwarfUtil. | Bernhard Schommer | 2014-10-24 | 1 | -0/+39 |
| | | | |||||
| * | | Added a file for utility functions on the Dwarf types. | Bernhard Schommer | 2014-10-23 | 2 | -42/+66 |
| | | | |||||
| * | | Added type for all tags. | Bernhard Schommer | 2014-10-21 | 1 | -1/+22 |
| | | | |||||
| * | | Fixed smaller mistakes. | Bernhard Schommer | 2014-10-21 | 1 | -8/+7 |
| | | | |||||
| * | | Removed more not needed attributes. | Bernhard Schommer | 2014-10-20 | 1 | -92/+32 |
| | | | |||||
| * | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-10-20 | 1 | -0/+1 |
| |\| | |||||
| | * | 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 more not needed attributes from the tag types. | Bernhard Schommer | 2014-10-17 | 1 | -19/+50 |
| | | | |||||
 |
index : compcert | |
| CompCert fork with minor modifications for Vericert. |
| aboutsummaryrefslogtreecommitdiffstats |