diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-06-08 08:32:53 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-06-08 08:32:53 +0200 |
| commit | 744dc278d24b15a72ef471fc25c1c8a8df62cc4e (patch) | |
| tree | 6d7340f815cf1c01d50e10313ae034a2821b6a2a /arm/Asm.v | |
| parent | 584eac7027cd4d29c5ca8744453ffeea8f18b501 (diff) | |
| parent | 1cdf4f22706dea5371f6d553538ac68f1f0a159f (diff) | |
| download | compcert-kvx-744dc278d24b15a72ef471fc25c1c8a8df62cc4e.tar.gz compcert-kvx-744dc278d24b15a72ef471fc25c1c8a8df62cc4e.zip | |
Merge pull request #43 from AbsInt/standard-headers
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.
Diffstat (limited to 'arm/Asm.v')
0 files changed, 0 insertions, 0 deletions