diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-04-25 10:58:56 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-25 10:58:56 +0200 |
commit | 760e4226be66e84ac538461f76e12fb925cb204c (patch) | |
tree | 2e81d00017ed23b0a8a5d6393829d1eb35a25ac8 /cparser/C.mli | |
parent | e34dc31ee4058c8df3ca92acb33fad153634792c (diff) | |
download | compcert-kvx-760e4226be66e84ac538461f76e12fb925cb204c.tar.gz compcert-kvx-760e4226be66e84ac538461f76e12fb925cb204c.zip |
Improved handling and diagnostics for the `auto` storage class (#99)
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.
Diffstat (limited to 'cparser/C.mli')
-rw-r--r-- | cparser/C.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/cparser/C.mli b/cparser/C.mli index cacdbe7c..d674afb8 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -85,9 +85,10 @@ type attributes = attribute list (** Storage classes *) type storage = - | Storage_default + | Storage_default (* used for toplevel names without explicit storage *) | Storage_extern | Storage_static + | Storage_auto (* used for block-scoped names without explicit storage *) | Storage_register (** Unary operators *) |