aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | | | | | | | | | | | | | | | | | | | | | | | | 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
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Changed the printer for the annotations in the Asm_printer of the checklink ↵Bernhard Schommer2015-04-141-4/+31
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | tool.
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | When using gcc as a preprocessor, put it in C99 mode.Xavier Leroy2015-04-101-6/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As opposed to the default "gnu99" mode, the C99 mode turns off a number of GNU-isms in standard header files like those of glibc.
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | Detect (and reject with an error) preprocessing numbers that are not valid ↵Xavier Leroy2015-04-061-0/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | integer or floating constants.
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | Harmless typo ('__' instead of '_') causing a warning at extraction time.Xavier Leroy2015-04-061-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | Missing case for the new 'annot' instruction.Xavier Leroy2015-04-062-0/+4
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixed missing unsigned compare for pointer in the arm backend.Bernhard Schommer2015-04-042-3/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | | | | | | Further updates to README.mdXavier Leroy2015-04-041-9/+18
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | | | | | Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2015-04-021-13/+8
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge pull request #36 from clarus/masterBernhard Schommer2015-04-021-13/+8
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Cosmetic: README in MarkDown
| | * | | | | | | | | | | | | | | | | | | | | | | | | | | README in MarkDownGuillaume Claret2015-04-021-13/+8
| |/ / / / / / / / / / / / / / / / / / / / / / / / / / /
* / / / / / / / / / / / / / / / / / / / / / / / / / / / Ccompuimm now depends on the memory, this is needed to proof the Lemma ↵Bernhard Schommer2015-04-021-2/+3
|/ / / / / / / / / / / / / / / / / / / / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | op_depends_on_memory_correct.
* | | | | | | | | | | | | | | | | | | | | | | | | | | Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-0171-516/+1736
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Extended annotations
| * | | | | | | | | | | | | | | | | | | | | | | | | | | Updating the PowerPC and ARM ports.Xavier Leroy2015-03-2712-96/+92
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | PowerPC: always use full register names to print annotations.
| * | | | | | | | | | | | | | | | | | | | | | | | | | | Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-2714-78/+130
| | | | | | | | | | | | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | | | | | | | | | | | Extended arguments to annotations, continued:Xavier Leroy2015-03-276-294/+142
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Simplifications in RTLgen. - Updated Cexec.
| * | | | | | | | | | | | | | | | | | | | | | | | | | | Extend annotations so that they can keep track of global variables and local ↵Xavier Leroy2015-03-2748-368/+1692
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | variables whose address is taken. - CminorSel, RTL: add "annot" instructions. - CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions. - AST, Events: simplify EF_annot because constants are now part of the arguments. Implementation is not complete yet.
* | | | | | | | | | | | | | | | | | | | | | | | | | | Merge pull request #31 from AbsInt/null-ptr-cmpXavier Leroy2015-04-0118-151/+226
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | Revised semantics of comparisons between a pointer and 0.
| * | | | | | | | | | | | | | | | | | | | | | | | | | Omission: forgot to treat pointer values in bool_of_val and sem_notbool.Xavier Leroy2015-03-2912-120/+182
| | | | | | | | | | | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | | | | | | | | | | Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-159-31/+44
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It used to be that a pointer value (Vptr) always compare unequal to the null pointer (Vint Int.zero). However, this may not be true in the final machine code when pointer addition overflows and wraps around to the bit pattern 0. This patch checks the validity of the pointer being compared with 0, and makes the comparison undefined if the pointer is out of bounds. Note: only the IA32 back-end was updated, ARM and PowerPC need updating.
* | | | | | | | | | | | | | | | | | | | | | | | | | Merge pull request #35 from jhjourdan/masterXavier Leroy2015-04-012-2/+2
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | Fix overflows in printers for clight and csyntax.
| * | | | | | | | | | | | | | | | | | | | | | | | | Fix overflows in printers for clight and csyntax.Jacques-Henri Jourdan2015-04-012-2/+2
|/ / / / / / / / / / / / / / / / / / / / / / / / /
* | | | | | | | | | | | | | | | | | | | | | | | | Merge pull request #33 from AbsInt/struct-passingXavier Leroy2015-03-3122-112/+1115
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | ABI conformance for passing function arguments and returning function results of struct and union types
| * | | | | | | | | | | | | | | | | | | | | | | | Support va_arg for vararg arguments of composite (struct/union) types.Xavier Leroy2015-03-202-0/+19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now for IA32 and PowerPC as well.
| * | | | | | | | | | | | | | | | | | | | | | | | Support va_arg for vararg arguments of composite (struct/union) types.Xavier Leroy2015-03-204-15/+67
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ARM is done, IA32 and PowerPC remain to be updated.
| * | | | | | | | | | | | | | | | | | | | | | | | "ecomma" smart constructor: reassociate to the left so that it prints more ↵Xavier Leroy2015-03-201-2/+8
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | nicely.
| * | | | | | | | | | | | | | | | | | | | | | | | Fix .type and .size annotations: @ is comment, use % instead.Xavier Leroy2015-03-201-2/+6
| | | | | | | | | | | | | | | | | | | | | | | | |