diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-03 11:48:37 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-06-04 16:32:12 +0200 |
| commit | ada3c2411aab46eb26753c428a0ca56c9adfc428 (patch) | |
| tree | d0e3e7ec9b79be427e4b03e03d20335a483cac05 /cparser/Diagnostics.mli | |
| parent | 130990b8c24db1ccc44dc1b85907904433351e8d (diff) | |
| download | compcert-kvx-ada3c2411aab46eb26753c428a0ca56c9adfc428.tar.gz compcert-kvx-ada3c2411aab46eb26753c428a0ca56c9adfc428.zip | |
Warn for defs and uses of static variables in nonstatic inline functions
Nonstatic inline functions can be expanded in several compilation units.
The static variables in question may differ between different expansions.
This is a manual merge and adaptation of pull request #P95 by @bschommer.
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 4f3aebe9..0d49cd0b 100644 --- a/cparser/Diagnostics.mli +++ b/cparser/Diagnostics.mli @@ -51,6 +51,7 @@ type warning_type = | Unused_ais_parameter (** unused builtin ais parameter *) | Ignored_attributes (** attributes declarations after definition *) | Extern_after_definition (** extern declaration after non-extern definition *) + | Static_in_inline (** static variable in non-static inline function *) 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 |