| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
| |
Bug 17392
|
|
|
|
|
|
|
|
|
|
| |
The gcc produces DW_AT_ranges for non-contiguous address ranges, like
compilation units containing functions which are placed in different
ELF-sections or lexical scopes that are split up. With this commit
CompCert also uses this DWARF v3 feature for gnu backend based targets.
In order to ensure backward compability a flag is added which avoids
this and produces debug info in DWARF v2 format.
Bug 17392.
|
|
|
|
|
|
|
|
|
| |
In contrast to the dcc, the gcc uses address ranges to express
non-contiguous range of addresses. As a first step we set the
start and end addresses for the different address ranges for
the compilation unit by using the start and end addresses of
functions.
Bug 17392.
|
|
|
|
| |
Bug 17392.
|
|
|
|
|
|
|
|
| |
Like, for example the clang, CompCert now prints a more detailed
descriptions of the debug information in the assembler file. For
each abbreviation and debug entry the dwarf attributes and their encodings
are added.
Bug 17392.
|
|
|
|
|
|
| |
Instead of pushing strings around use the actual section. However
the string is still used in the Hashtbl.
Bug 17392.
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
Instead of using a string they now take an optional string, which
should be none if the backend is not the diab backend and the
corresponding section is the text section and Some s with s being
the custom section name else.
Bug 17392.
|
|
|
|
|
|
|
|
| |
GCC prints all string larger than 3 characters in the debug_str
section which reduces the size of the debug information since entries
containing the same string now map to the same string in the
debug_str sections.
Bug 17392.
|
|
|
|
|
|
|
| |
The dwarf 2 standard allows more attributes for certain debuggint
entries than used by gcc or diab data. Since they are also not
set by compcert they can be removed.
Bug 17392.
|
|
|
|
|
| |
The function exists_type is not really used so we can remove it.
Bug 17392.
|
|
|
|
|
|
|
| |
Instead of making each filed mutuable we use a reference to a record
of type implem. Now only the default implementation and the default
debug information need to be upated to add a new function.
Bug 17392.
|
|
|
|
|
|
| |
Instead of using a tuple we now use a record with descriptive names
for the different entries.
Bug 17392
|
|
|
|
|
|
| |
Since the strip functions might be useful in other context and is
more general then the debug information.
Bug 17392.
|
|
|
|
|
|
| |
The atom to global variable debug id mapping is never used so we
do not need to insert global variables into it.
Bug 17392.
|
|
|
|
|
|
|
| |
Instead of defining two functions for adding the mapping from atom
to debug id we use one function which then sets the corresponding
values.
Bug 17392.
|
| |
|
|
|
|
|
|
| |
If a label is printed before a list of debug annotations we can use it
for the debug annotations and don't need to add an extra label.
Bug 17392
|
|
|
|
|
| |
The base register for the stack allocated variables should be
r1 and not r2 under powerpc. Bug 17392
|
| |
|
|\
| |
| | |
Take advantage of PowerPC 64-bit instructions
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| |\ \
| |/ /
|/| /
| |/ |
Resolved conflicts in:configure powerpc/Asmexpand.ml
|
| | |
|
|\ \
| | |
| | | |
Upgrade to Flocq 2.5.0.
|
| | |
| | |
| | |
| | | |
Note: this version of Flocq is compatible with both Coq 8.4 and 8.5.
|
| | |
| | |
| | |
| | |
| | |
| | | |
Like for arm and ppc the functions for section names and start and
end addresses of compilation units are defined and the print_annot
function is moved to Asmexpandaux.ml.
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
The name_of_section function no returns the correct name for the
debug sections, the prologue and epilogue directives are added and
the labels for the live ranges are introduced in the Asmexpand pass.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
taking the ident as argument.
This functions are currently not used inside the proven part but it
is nice to have them already there, when they are used by some future
pass. They also come equiped with the corresponding proofs.
|
| | |
| | |
| | |
| | |
| | |
| | | |
The function is generalized to work for all backends and takes as
additional arguments functions for the printing of the simple
instructions and the translation function for the arguments.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | | |
handled as a function with void parameter.
|
|\ \ \ |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | | |
information.
|
| | | |
| | | |
| | | |
| | | |
| | | | |
C11 allows a typedef redefinition if the types are the same.
We now allow this also and issue a warning and an error if the types are different.
|
|/ / / |
|
| | | |
|
| | | |
|
|\ \ \
| | | |
| | | |
| | | |
| | | | |
Conflicts:
debug/DebugInformation.ml
|
| | | | |
|
| | | | |
|