aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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
| |
* | Merge branch 'master' into dwarfBernhard Schommer2014-11-1712-179/+489
|\|
| * Add flags to control individual optimization passes + flag -O0 for turning ↵Xavier Leroy2014-11-167-46/+128
| | | | | | | | them off.
| * Revised parsing of command-line arguments (in preparation for adding more).Xavier Leroy2014-11-163-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 Leroy2014-11-151-15/+86
| |
| * cchecklink: added option "-files-from" to read .sdump file namesXavier Leroy2014-11-152-4/+29
| | | | | | | | from a file or from standard input.
* | Removed compile error and added dummy function for the printing of entries.Bernhard Schommer2014-11-173-8/+12
| |
* | More functionality for the Printer.Bernhard Schommer2014-11-141-1/+4
| |
* | Moved abbreviation printer into a seperate file. The printer should also ↵Bernhard Schommer2014-11-123-325/+394
| | | | | | | | print the debug info.
* | Added functions for printing of the abbreviations.Bernhard Schommer2014-11-113-3/+41
| |
* | Generalised functionality for the printing of the abbreviations.Bernhard Schommer2014-11-112-235/+307
| |
* | Added more functions to print the abbreviations.Bernhard Schommer2014-11-062-99/+167
| |
* | More functions for printing the abbreviations.Bernhard Schommer2014-10-312-77/+141
| |
* | Reverted changes to C2C since the information needed should be stored ↵Bernhard Schommer2014-10-301-16/+4
| | | | | | | | already earlier.
* | Started implementing functions to compute the abbreviations for the diab ↵Bernhard Schommer2014-10-292-13/+87
| | | | | | | | compiler.
* | Refactored the printing functions a little bit more by moving the system ↵Bernhard Schommer2014-10-284-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 Schommer2014-10-272-5/+20
| |
* | Merge branch 'master' into dwarfBernhard Schommer2014-10-272-2/+3
|\|
| * Tune behavior wrt warnings:Xavier Leroy2014-10-242-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 Schommer2014-10-241-0/+39
| |
* | Added a file for utility functions on the Dwarf types.Bernhard Schommer2014-10-232-42/+66
| |
* | Added type for all tags.Bernhard Schommer2014-10-211-1/+22
| |
* | Fixed smaller mistakes.Bernhard Schommer2014-10-211-8/+7
| |
* | Removed more not needed attributes.Bernhard Schommer2014-10-201-92/+32
| |
* | Merge branch 'master' into dwarfBernhard Schommer2014-10-201-0/+1
|\|
| * Deactivated the warning for deprecated features for compilation of ↵Bernhard Schommer2014-10-201-0/+1
| | | | | | | | cchecklink since it breaks the build with newer ocaml versions.
* | Removed more not needed attributes from the tag types.Bernhard Schommer2014-10-171-19/+50
| |
* | Merge branch 'master' into dwarfBernhard Schommer2014-10-171-1/+0
|\|
| * Removed duplicated open.Bernhard Schommer2014-10-171-1/+0
| |
* | Started revising the tag types to only include attributes which are actually ↵Bernhard Schommer2014-10-151-17/+10
| | | | | | | | used debuggers.
* | Added the rest of the type for the tags mentioned in appendix 1 of the dwarf ↵Bernhard Schommer2014-10-151-1/+56
| | | | | | | | 2 standard.
* | Added more types.Bernhard Schommer2014-10-141-0/+125
| |
* | Added a file containing definitions for the types used to store the debug ↵Bernhard Schommer2014-10-132-1/+122
|/ | | | information. The types follow the Current Attributes by Tag Value in Appendix 1 of the Dwarf 2 standard.
* Revised translation of '&&' and '||' to Clight.Xavier Leroy2014-10-1311-124/+109
| | | | | | | | | | | The previous translation (in SimplExpr) produced references to the same temporary variable with two different types (bool and int), which is not nice if we want to typecheck the generated Clight. The new translation avoids this and also gets rid of the double cast to bool then to int. The trick is to change Eparen (in CompCert C expressions) to take two types: the type to which the argument must be converted, and the type with which the resulting expression is seen.
* Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0.Xavier Leroy2014-10-093-1/+3
|
* Merge pull request #1 from jhjourdan/masterXavier Leroy2014-10-0921-942/+6030
|\ | | | | Upgrade to flocq 2.4.0
| * Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-0721-942/+6030
| |
* | Refactored the code of ia32/PrintAsm.ml by moving the functions depending on ↵Bernhard Schommer2014-10-081-138/+220
| | | | | | | | the target system in a seperate module.
generated by cgit (git 2.34.1) at 2024-07-05 13:19:58 +0000