diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-05-07 17:21:55 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-07 17:21:55 +0200 |
| commit | e2c2f22be7e4df4ceb9a4c7e6c1695d0aeef7865 (patch) | |
| tree | 6ba8c18b1de5983363826645eed123aca5702220 /cparser/Diagnostics.mli | |
| parent | 6657ff7f757d22ad70fe13458f8e7eb76698ac6b (diff) | |
| download | compcert-kvx-e2c2f22be7e4df4ceb9a4c7e6c1695d0aeef7865.tar.gz compcert-kvx-e2c2f22be7e4df4ceb9a4c7e6c1695d0aeef7865.zip | |
Added a diagnostic for attributes dec after def
The new warning is raise for function declaration after a function
definition that introduce new attributes, which are ignored.
Bug 23385
Diffstat (limited to 'cparser/Diagnostics.mli')
| -rw-r--r-- | cparser/Diagnostics.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli index 75865cb2..ea8f2159 100644 --- a/cparser/Diagnostics.mli +++ b/cparser/Diagnostics.mli @@ -49,6 +49,7 @@ type warning_type = | Unused_parameter (** unused function parameter *) | Wrong_ais_parameter (** wrong parameter type for ais replacement *) | Unused_ais_parameter (** unused builtin ais parameter *) + | Ignored_attributes (** attributes declarations after 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 |