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 | |
| 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')
| -rw-r--r-- | cparser/Diagnostics.ml | 6 | ||||
| -rw-r--r-- | cparser/Diagnostics.mli | 1 | ||||
| -rw-r--r-- | cparser/Elab.ml | 5 |
3 files changed, 11 insertions, 1 deletions
diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml index d014921a..91acd161 100644 --- a/cparser/Diagnostics.ml +++ b/cparser/Diagnostics.ml @@ -93,6 +93,7 @@ type warning_type = | Wrong_ais_parameter | Unused_ais_parameter | Ignored_attributes + | Extern_after_definition (* List of active warnings *) let active_warnings: warning_type list ref = ref [ @@ -116,6 +117,7 @@ let active_warnings: warning_type list ref = ref [ Wrong_ais_parameter; Unused_ais_parameter; Ignored_attributes; + Extern_after_definition; ] (* List of errors treated as warning *) @@ -148,6 +150,7 @@ let string_of_warning = function | Wrong_ais_parameter -> "wrong-ais-parameter" | Unused_ais_parameter -> "unused-ais-parameter" | Ignored_attributes -> "ignored-attributes" + | Extern_after_definition -> "extern-after-definition" (* Activate the given warning *) let activate_warning w () = @@ -196,6 +199,7 @@ let wall () = Unused_parameter; Wrong_ais_parameter; Ignored_attributes; + Extern_after_definition; ] let wnothing () = @@ -228,6 +232,7 @@ let werror () = Wrong_ais_parameter; Unused_ais_parameter; Ignored_attributes; + Extern_after_definition; ] (* Generate the warning key for the message *) @@ -407,6 +412,7 @@ let warning_options = error_option Wrong_ais_parameter @ error_option Unused_ais_parameter @ error_option Ignored_attributes @ + error_option Extern_after_definition @ [Exact ("-Wfatal-errors"), Set error_fatal; Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *) Exact ("-fno-diagnostics-color"), Unset color_diagnostics; diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli index ea8f2159..4f3aebe9 100644 --- a/cparser/Diagnostics.mli +++ b/cparser/Diagnostics.mli @@ -50,6 +50,7 @@ type warning_type = | Wrong_ais_parameter (** wrong parameter type for ais replacement *) | Unused_ais_parameter (** unused builtin ais parameter *) | Ignored_attributes (** attributes declarations after definition *) + | Extern_after_definition (** extern declaration after non-extern definition *) val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a (** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to 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 |