| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
| |
Ranges of locations are relative to some base address. Most times
this is just the same as the compilation unit. However if the
compilation unit contains functions in multiple sections we need
to add a base address of the section that the locations are
contained.
|
|
|
|
|
|
|
|
| |
debug/DwarfPrinter.mli: unused functor parameter trigger warning 69,
replace by non-dependent functor type.
Makefile.extr: turn warning 69 (unused functor parameter) off
for extracted code
configure: accept OCaml versions above 4.09
configure: update messages for unsupported versions of OCaml and Coq
|
|
|
|
|
|
|
|
|
| |
Move its definitions to modules C (the type `builtins`) and Env
(the operations that deal with the initial environment).
Reasons for the refactoring:
1- The name "Builtins" will soon be reused for a Coq module
2- `Env.initial()` makes more sense than `Builtins.environment()`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Do not use `Pervasives.xxx` qualified names
Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`,
and uses of `Pervasives` cause fatal warnings.
This commit uses unqualified names instead, as no ambiguity occurs.
* Clarify "open" statements
OCaml 4.08.0 has stricter warnings concerning open statements that
shadow module names.
Closes: #300
|
|
|
|
|
|
| |
This is a manual, partial merge of Github pull request #296 by @Fourchaux.
flocq/, cparser/MenhirLib/ and parts of test/ have not been changed
because these are local copies and the fixes should be performed upstream.
|
|
|
|
|
| |
The AbsInt build number no longer contains "release", so it must
be printed additionally.
|
|
|
|
|
|
|
| |
Instead of printing an the start label and adding the offset by
computing the difference of the range label and the start label
use the range label directly.
Bug 26234
|
|
|
|
|
|
|
|
|
|
|
| |
Functions that are removed from the compilation unit, for example
inline functions without extern, should not produce debug
information.
This commit reuses the mechanism used for variables in order to
track additionally the printed functions. Therefore the printed
variable versions are exchanged for a printed symbol version.
Bug 26234
|
|
|
|
|
|
|
|
|
|
|
|
| |
The fist changes changes the offset for range entries to used labels
instead of integer constants, leaving the computation to the
assembler.
The second part of the change the address changes the way ranges
entries of scopes are printed. They need to be relative to the start
address of the code in the section they are included.
Bug 26234
|
|
|
|
|
|
| |
As noted in the DWARF 3 specification empty ranges have no effect
and can be left out.
Bug 26234
|
|
|
|
|
|
| |
Ranges for non-contiguous address ranges are already part of dwarf
version 3.
Bug 26234
|
|
|
|
|
|
| |
Fix various typos in diagnostic messages and unified wording and
capitalization.
Bug 23850
|
| |
|
|
|
|
|
|
| |
We don't need verbose debug for the assembler. The verbose debug
information should only be printed if assembler files are
generated.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.
The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.
In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.
|
|
|
|
|
|
| |
Instead of using Filename.quote, string entries are printed with
%S.
Bug 21216
|
|
|
|
|
|
| |
The compilation directory entry needs quoting since it could be
a toplevel directory under windows.
Bug 21216
|
|
|
|
|
|
|
| |
The variable gnu_toolchain is true if a gnu toolchain is used and
false in all other cases. The variable avoids the explicit test
whether the system string is diab and should be easier to change.
Bug 20521.
|
|
|
|
|
| |
Instead of exporting and setting all functions we just fill the
struct already in DebugInformation with the correct functions.
|
|
|
|
| |
The two types needed from AST are prefixed directly.
|
|
|
|
|
| |
Only two types from AST are needed and the global shadowing open
can be removed.
|
|
|
|
|
| |
Anonymous members no longer are printed in the debug information.
Fix 20798
|
|
|
|
|
|
| |
Instead of escaping all newlines etc for the help options use
quoted strings.
Bug 19872
|
| |
|
|
|
|
|
| |
The arm dwarf float registers constants are larger than 2 bytes.
Bug 20489
|
|
|
|
|
| |
A non reseted Hashtbl caused problems with multiple input files.
Bug 20462
|
|
|
|
|
|
| |
Since the dwarf register names for x86_32 and x86_64 differ it is
wrong to hardcode the dwarf register number for rsp to 4.
Bug 20461
|
|
|
|
|
| |
Address constants need to be 64bit also in the debug information.
Bug 20335
|
| |
|
| |
|
|
|
|
|
|
|
| |
The options controlling the generation of debugging information
are now moved into the Debug module. Futhermore the -gdepth
options are replaced in favor of a more gcc compatible version.
Bug 20193
|
| |
|
| |
|
|
|
|
|
|
| |
The configuration advanced debug is removed and now full debug
information is also generated for ia32 and arm.
Bug 17609
|
|\ |
|
| |
| |
| |
| |
| |
| | |
The interface hides the implementation details, like the huge
number of Hashtbls from the rest of the implementatio.
Bug 18394
|
|/
|
|
|
|
| |
Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
|
|
|
|
|
|
| |
The typdef, enumerator and function_type types form the DebugTypes and
DwarfTypes shared a some fields. This commits renames them in order to
make them more unique and avoid potential name clashes.
|
|
|
|
|
|
| |
In order to get deterministic output code we need to sort the strings
in the debug_str section by their label.
Fix 17727.
|
|
|
|
|
|
|
| |
Since the identifier of a function definition and of its declaration
are equal we only should remove functions if the function iteself is
removed.
Bug 17724.
|
|
|
|
|
|
|
|
|
|
|
| |
The new option gdepth subumes the gonly-globals. The option
allows it to control the level of information that is produced.
This option allows it to generate debugging inforation for:
-Only globals
-Global and local variables but without location information for
the local variable
-Full information
Bug 17638.
|
|
|
|
|
|
|
| |
In the case of struct function parameters it is not always
guaranteed that they are still there and not translated into plain
integer arguments.
Bug 17609.
|
|\
| |
| |
| | |
git+ssh://ssh.absint.com/common/repositories/git/tools/compcert
|
| |
| |
| |
| |
| |
| |
| | |
For function types used by function pointers we do not need to print
the name of the paraments. Also switch the logic in case of
prototyped/unprototyped.
Fix 17579.
|
|/ |
|
|
|
|
|
|
| |
The new option -gonly-global allows the generation of debuging
information for global variables only.
Bug 17566.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
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.
|