diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2019-09-25 16:45:42 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-09-25 16:45:42 +0200 |
| commit | b5b154620e454ba947957eb1164acbffff1cb5bd (patch) | |
| tree | c6180d5a9cd2fcc8a193b62b19a0338998e022a9 /cparser | |
| parent | f1637021cd51505796e878a21d1b30df0b42e236 (diff) | |
| download | compcert-kvx-b5b154620e454ba947957eb1164acbffff1cb5bd.tar.gz compcert-kvx-b5b154620e454ba947957eb1164acbffff1cb5bd.zip | |
Functions that are extern should stay extern (#201)
In ISO C, inline functions behaves differently whether they have been declared `extern` at least once or not (i.e. all the declarations have no `extern` and no `static` modifier).
Hence, functions that have been declared / defined `extern` once should remain `extern` when redeclared without `extern`. This gives the ISO C behavior for inline functions and has no impact for non-inline functions.
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 3797164d..50346324 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -172,7 +172,7 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = error loc "static declaration of '%s' follows non-static declaration" s; sto | Storage_static,_ -> Storage_static (* Static stays static *) - | Storage_extern,_ -> sto + | Storage_extern,_ -> if is_function_type env new_ty then Storage_extern else sto | 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"; |