| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
folded away prior.
|
| | | | |\ \ \ \ \ \ |
|
| | | | |\ \ \ \ \ \ \ |
|
| | | | | | | | | | | | |
|
| |_|/ / / / / / / / /
|/| | | | | | | | | | |
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing
changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \
| | | |_|_|_|_|_|_|_|_|/
| | |/| | | | | | | | | |
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
the same way as it is done for PPC.
|
| | | | | | | | | | | | |
|
| |_|_|/ / / / / / / /
|/| | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | |
|
|/ / / / / / / / / / /
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
an switch to bail out on earlier on unstructured switch.
|
| |_|/ / / / / / / /
|/| | | | | | | | | |
|
| |/ / / / / / / /
|/| | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Otherwise we get too many errors on glibc's standard headers.
A real error will occur when the anonymous struct/union is accessed.
|
| | | | | | | | | |
|
| | | | | | | | | |
|
|/ / / / / / / / |
|
|\ \ \ \ \ \ \ \
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
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.
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
variable is redefined as a typedef.
|
| | | | | | | | |
|
| |_|_|_|_|_|/
|/| | | | | |
| | | | | | |
| | | | | | | |
with different build systems.
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
"old-style" unprototyped.
Use this info in printing function types for Csyntax and Clight.
|
| |_|_|_|_|/
|/| | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Ctyping: define a typechecker for whole programs.
Csyntax: introduce the type "pre-program" (non-dependent).
C2C: use Ctyping.econdition instead of Ctyping.econdition'.
Note: Ctyping.typecheck_program could be used as the first step
in the verified compilation pipeline. Then, retyping would
no longer be performed in C2C. We keep it this way (for the time
being) because retyping errors are reported more precisely in C2C than
in Ctyping.
|
| |_|_|_|/
|/| | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
non-static declaration is followed by a static declaration/definition.
|
| | | | | |
|
| |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- Treat clobbered registers as being destroyed by EF_inline_asm builtins
(which is the truth, semantically).
- To enable the above, represent clobbers as Coq strings rather than idents
and move register_by_name from Machregsaux.ml to Machregs.v.
- Side benefit: more efficient implementation of Machregsaux.name_of_register.
-# Please enter the commit message for your changes. Lines starting
|
| | | | |
|
| |_|/
|/| | |
|
| | |
| | |
| | |
| | | |
Val.lessdef, etc.
|
| | |
| | |
| | |
| | | |
and produce a diagnostic instead of ignoring them.
|
| | |
| | |
| | |
| | | |
bit field.
|
| | |
| | |
| | |
| | | |
unblocking; improve translation of bitfield initializers and compound literals.
|
|/ /
| |
| |
| |
| |
| | |
Bitfields: better translation of initializers and compound literals; run this pass before unblocking.
Transform.stmt: extend with ability to treat unblocked code.
test/regression: more bitfield tests.
|
|/
|
|
|
|
| |
(underflow).
Also: spurious '\n' in C2C.warning.
|
|
|
|
| |
clobber lists.
|