| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
| |
cfrontend/C2C.ml
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The Elab pass checks that the argument of 'case' is a compile-time constant
expression. This commit records the value of this expression in the
C.Scase AST generated by Elab, so that it can be used for further
diagnostics, i.e. checking (in Elab) for duplicate cases.
Note that C2C ignores the recorded value and recomputes the value of
the expression using Ceval.integer_expr. This is intentional:
Ceval.integer_expr is more trustworthy, as it is formally verified
against the CompCert C semantics.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Previously, CompCert would just ignore the `auto` keyword, thus accepting
incorrect top-level definitions such as
```
auto int x;
auto void f(auto int x) { }
```
This commit introduces `auto` as a proper storage class
(Storage_auto constructor in the C AST).
It adds diagnostics for misuses of `auto`, often patterned after the
existing diagnostics for misuses of `register`.
Some error messages were corrected ("storage-class" -> "storage class")
or made closer to those of clang.
Finally, in the generated C AST and in C typing environments,
block-scoped variables without an explicit storage class are recorded
as Storage_auto instead of Storage_default. This is semantically correct
(block-scoped variables default to `auto` behavior) and will help us
distinguishing block-scoped variables from file-scoped variables
in later developments.
|
| |
|
|
|
|
| |
This part of PR#81 causes problems with long double static variables
in math.h. Revert to the old behavior of not including static
variables unless actually referenced.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(#81)
* Added check for redefinition of globals.
Since Cleanup may remove duplicated static functions or global
definitions we need to check for duplication during elaboration,
not just in C2C.
Bug 23410
* Do not eliminate unreferenced static variables with initializers
This way all initialized variables make it to the C2C pass,
where the initializers are checked for constant-ness.
Bug 23410
|
| |
|
|
|
|
|
| |
Since the identifier of a function definition and of its declaration
are equal we only should remove functions if the function iteself is
removed.
Bug 17724.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
| |
- Support for empty structs and unions
- Better handling of "extern" and "extern inline" function definitions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2493 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2353 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
| |
cparser: add primitive support for enum types.
bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
|
|
| |
and __alignof__(ty), __alignof__(expr) from GCC.
- Resurrected __builtin_memcpy_aligned, useful for files generated
by Scade KCG 6.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1827 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
| |
cparser: added experimental emulation of packed structs (PackedStruct.ml)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
