| Commit message (Collapse) | Author | Age | Files | Lines |
|\
| |
| |
| |
| | |
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.
|
|
|
|
|
| |
Restrict pointer event values to public global names.
Update proofs accordingly. PowerPC and ARM need updating.
|
|
|
|
| |
For the moment, this field is ignored.
|
|
|
|
| |
them off.
|
|
|
|
|
|
| |
Honor "ccomp -E foo.h" for GCC compatibility.
Accept .o.ext files as object files for GCC compatibility.
Fixed and improved handling of Cminor source files.
|
|
|
|
|
|
|
|
|
|
|
| |
The previous translation (in SimplExpr) produced references to the
same temporary variable with two different types (bool and int),
which is not nice if we want to typecheck the generated Clight.
The new translation avoids this and also gets rid of the double
cast to bool then to int. The trick is to change Eparen
(in CompCert C expressions) to take two types: the type to which the
argument must be converted, and the type with which the resulting
expression is seen.
|
|
|
|
| |
for the configuration file.
|
|
|
|
| |
including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
|
| |
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2572 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2564 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
ARM: various tweaks, incl. support for SDIV and UDIV insns when available.
test/regression/funptr2.c: Thumb does weird things with <function ptr>+1.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|