aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cleanup.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2018-04-25 10:58:56 +0200
committerGitHub <noreply@github.com>2018-04-25 10:58:56 +0200
commit760e4226be66e84ac538461f76e12fb925cb204c (patch)
tree2e81d00017ed23b0a8a5d6393829d1eb35a25ac8 /cparser/Cleanup.ml
parente34dc31ee4058c8df3ca92acb33fad153634792c (diff)
downloadcompcert-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/Cleanup.ml')
-rw-r--r--cparser/Cleanup.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index c10eeb55..9568d8fe 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -134,7 +134,7 @@ let visible_fundef f =
| Storage_default -> not f.fd_inline
| Storage_extern -> true
| Storage_static -> false
- | Storage_register -> assert false
+ | Storage_auto | Storage_register -> assert false
let rec add_init_globdecls accu = function
| [] -> accu