From 760e4226be66e84ac538461f76e12fb925cb204c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 25 Apr 2018 10:58:56 +0200 Subject: 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. --- cparser/C.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'cparser/C.mli') 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 *) -- cgit