| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| | |
|
| |
| |
| |
| |
| |
| | |
This option allows it to specify a .ini file that is in the usual
search path.
Bug 17431
|
| |
| |
| |
| |
| |
| |
| |
| | |
The tools now can be specified by 3 ways:
-Relative to the compcert.ini file
-With absolute path to the location
-As a simple filename which lies on the PATH variable.
Bug 17431
|
| |
| |
| |
| |
| |
| | |
The path to the libcompert folder can be specified relative to the
location of the compcert.ini file.
Bug 17431
|
|/
|
|
|
|
| |
- Rename '-fstruct-return' into '-fstruct-passing', because this emulation affects both function result passing and function argument passing. Keep '-fstruct-return' as a deprecated synonymous for '-fstruct-passing'
- Remove the ability to change the ABI for struct passing via the '-fstruct-passing=<abi>' and '-fstruct-return=<abi>' command-line flags. This was more confusing than useful.
- Produce an error if a struct/union is passed as function argument and '-fstruct-passing' is not set. This used to be supported, using CompCert's default ABI for passing struct arguments. However, this default ABI does not match any of the standard ABIs of our target platforms, so it is better to reject than to silently produce ABI-incompatible code.
|
|
|
|
|
| |
The option --conf allows it to overwrite the compcert.ini file.
Bug 17431.
|
|
|
|
|
|
| |
The diab backend calls the assembler directly and does not call
the compiler like for the gcc based backends.
Fix 17668.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
Sometimes, Unix.waitpid returns early with a EINTR error code, e.g. if a signal was handled. (Observed while running ccomp under the lldb debugger in MacOS X). Just restart Unix.waitpid in this case.
|
|
|
|
|
|
| |
The new option -gonly-global allows the generation of debuging
information for global variables only.
Bug 17566.
|
|
|
|
|
|
|
|
| |
file.
The new option -sdump-suffix allows it to specify another suffix
for the sdump file.
Bug 17326
|
|\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Conflicts:
arm/TargetPrinter.ml
backend/CMparser.mly
backend/SelectLongproof.v
backend/Selectionproof.v
cfrontend/C2C.ml
checklink/Asm_printers.ml
checklink/Check.ml
checklink/Fuzz.ml
common/AST.v
debug/DebugInformation.ml
debug/DebugInit.ml
debug/DwarfPrinter.ml
debug/DwarfTypes.mli
debug/Dwarfgen.ml
exportclight/ExportClight.ml
ia32/TargetPrinter.ml
powerpc/Asm.v
powerpc/SelectOpproof.v
powerpc/TargetPrinter.ml
|
| |
| |
| |
| | |
Bug 16529.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| | |
|
| | |
|
|/
|
|
|
|
|
|
|
|
| |
The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example:
* in $ARCH/Machregs.v to define the register conventions for builtin functions;
* in the VST program logic from Princeton to treat thread primitives specially.
So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq.
This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
|
| |
|
|
|
|
|
|
|
| |
In order to remove unnecessary dependecies the implemenation type is made
and the DebugInit file initializes the fields in the record. This allows
it to move more functions behind the Debug interface without introducing
circular dependencies.
|
|
|
|
|
|
| |
Added functions to add more information to the debuging interface,
like the struct layout with offsets, bitifiled layout and removed
the no longer needed mapping from stamp to atom.
|
|
|
|
|
|
|
|
| |
The new file Debug.ml contains the interface for generating and
printing debug information. In order to generate debug information
the init function initializes the necessary functions depending
on the -g flag. If the -g is not there all functions are dummy
functions which do nothing.
|
|\ |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
SimplLocals:
- record locations of stack-allocated variables with annotations
(of kind 5) at the beginning of the function;
- mark every assignment to non-stack-allocated variables with an
annotation of kind 2.
Debugvar: (new pass!)
- perform availability analysis for debug annotations of kind 2
- insert "start of live range" and "end of live range" annotations
(kind 3 and 4) to delimit intervals of PCs where the location
of a local variable is known.
|
| | |
|
| |
| |
| |
| | |
The diab compiler expected -Wm<pathname> without whitespace.
|
| |
| |
| |
| | |
warning about no input.
|
| | |
|
|/
|
|
| |
replaced the if else for the different possibilities by a List.find.
|
| |
|
|
|
|
| |
produced code in later checks.
|
| |
|
|\
| |
| |
| |
| | |
Conflicts:
driver/Driver.ml
|
| | |
|
| |
| |
| |
| | |
separate file.
|
| | |
|
|\| |
|
| |\
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Merge of the "standard-headers" branch. This provides CompCert-compatible implementations of the following standard headers: float.h, stdarg.h, stdbool.h, stddef.h, varargs.h.
These are the headers that are provided by GCC, Clang, and TCC. Other standard headers are provided by Glibc and similar C standard libraries.
So far in CompCert we rely on the headers provided by whatever C compiler is installed on the host platform. This causes some difficulties that this branch addresses:
1- Diab C's stdarg.h is not compatible with CompCert
2- On IA32 and PowerPC, CompCert's "long double" type differs from the "long double" type specified by the ABI. Hence, the platform's float.h gives "long double" parameters that do not match CompCert.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This branch provides implementations of the following standard headers:
<float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h>
These are the headers that are provided by GCC and Clang, as opposed
to being provided by Glibc and similar C standard libraries.
Configuration flag "-no-standard-headers" deactivates the installation
and use of these headers.
Lightly tested so far (IA32 Linux).
|
| | |
| | |
| | |
| | | |
As noticed by R. Krebbers, an inductive type for external worlds implies that all sequences of program-world interactions are finite, which is not the case.
|
| |/
| |
| |
| | |
with different build systems.
|
| | |
|
| |
| |
| |
| | |
unused information from the json dump.
|
|/ |
|
| |
|
|\
| |
| |
| |
| |
| | |
Conflicts:
Makefile
driver/Driver.ml
|
| |
| |
| |
| |
| |
| |
| |
| | |
composites).
- Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD.
- Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions.
- More comprehensive interoperability test in regression/interop1.c.
|
| |\ |
|