diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-05-07 20:09:54 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-05-26 11:05:13 +0200 |
| commit | 2b2585f39000f7000f296bc5b35c14e70f0c31fe (patch) | |
| tree | f7b8f8a520d65af2fb7bc94332e7760bae1eb032 /cparser/Elab.ml | |
| parent | 3de896cebebbdb35d179d17133ee53e505b1f0a8 (diff) | |
| download | compcert-kvx-2b2585f39000f7000f296bc5b35c14e70f0c31fe.tar.gz compcert-kvx-2b2585f39000f7000f296bc5b35c14e70f0c31fe.zip | |
Warning for extern declaration after definition.
Warning for change of storage class after the definition of a function
from default storage class to extern storage class. This only plays a
role if the function is also declared inline, since for inline functions
with default storage class no code is generated, but for inline functions
with extern storage class code should be generated.
Bug 23512
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 91d88e78..dd404d38 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -173,7 +173,10 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = sto | Storage_static,_ -> Storage_static (* Static stays static *) | Storage_extern,_ -> sto - | Storage_default,Storage_extern -> Storage_extern + | Storage_default,Storage_extern -> + if is_global_defined s && is_function_type env ty then + warning loc Extern_after_definition "this extern declaration follows a non-extern definition and is ignored"; + Storage_extern | _,Storage_extern -> old_sto (* "auto" and "register" don't appear in toplevel definitions. Normally this was checked earlier. Generate error message |