| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
configure: special ABI value for IA32/MacOSX and PowerPC/Linux
cparser/Machine: special config for PowerPC/Linux
cparser/StructReturn: generate better code for return-as-int
driver/Clflags, driver/Driver: add options -fstruct-return=<convention>
and -fstruct-passing=<convention> to simplify testing
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The passing of struct/union arguments by value implemented in the verified
part of CompCert is not compatible with the ARM, PowerPC and x86 ABI.
Here we enrich the StructReturn source-to-source emulation pass
so that it implements the calling conventions defined in these ABIs.
Plus: for x86, implement the returning of struct/union results by value
in a way compatible with the ABI.
|
| | |
| | |
| | |
| | | |
printing of packed structs.
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | | |
global target dependend option to activate the printing only for targets wher it works.
|
|\ \ \
| | |/
| |/| |
|
| |\ \ |
|
| | |/
| | |
| | |
| | |
| | |
| | | |
Cexec: record names of rules used in every reduction.
Interp: print these rule names in -trace mode. Also: simplified the exploration in "-all" mode; give unique names to states.
Csem: fix name of reduction rule "red_call".
|
| | | |
|
|\ \ \
| | |/
| |/| |
|
| |\ \
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- Switch CompCert C / Clight AST of composite types (structs and unions)
from a structural representation to a nominal representation,
closer to concrete syntax.
- This avoids algorithmic inefficiencies due to the structural representation.
- Closes PR#4.
- Smallstep: make small-step semantics more polymorphic in the type of the
global environment.
- Globalenvs: introduce Senv.t (symbol environments) as a restricted view
on Genv.t (full global environments).
- Events, Smallstep: use Senv instead of Genv to talk about global names.
|
| | | | |
|
| | | |
| | | |
| | | |
| | | | |
environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
|
|\| | |
| | | |
| | | |
| | | |
| | | | |
Conflicts:
powerpc/PrintAsm.ml
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Plus: simplify handling of -help and --help.
Plus: error on unrecognized "-xxx" options so that "-foo.c" is not treated
as a source file.
|
| | |/
| |/| |
|
|\| |
| | |
| | |
| | |
| | | |
Conflicts:
powerpc/PrintAsm.ml
|
| | | |
|
|\| | |
|
| |/
| |
| |
| | |
directory. Use Sys.executable_name instead of Sys.argv.(0).
|
|/
|
|
| |
-g option to the assembler.
|
|
|
|
| |
definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
|