aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2022-09-04 19:10:26 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2022-09-23 13:55:44 +0200
commit32910495644e7f6fbf9b3b85ecc16f4e30447e60 (patch)
tree81109ee811c3cf76c26b4741fee587133cee301e
parent9785a3cc148ad93dba1ea153f3390d6aab514755 (diff)
downloadcompcert-32910495644e7f6fbf9b3b85ecc16f4e30447e60.tar.gz
compcert-32910495644e7f6fbf9b3b85ecc16f4e30447e60.zip
Export the functions that control warnings
Activation and deactivation of a given warning, plus set-as-error and remove-as-error.
-rw-r--r--cparser/Diagnostics.mli13
1 files changed, 13 insertions, 0 deletions
diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli
index 47727707..e7d6fa0f 100644
--- a/cparser/Diagnostics.mli
+++ b/cparser/Diagnostics.mli
@@ -101,3 +101,16 @@ val error_summary : unit -> unit
val active_warning : warning_type -> bool
(** Test whether a warning is active to avoid costly checks *)
+
+val activate_warning : warning_type -> unit -> unit
+(** Turn the given warning on *)
+
+val deactivate_warning : warning_type -> unit -> unit
+(** Turn the given warning off *)
+
+val warning_as_error : warning_type -> unit -> unit
+(** Turn the given warning on and report it as an error *)
+
+val warning_not_as_error : warning_type -> unit -> unit
+(** Do not report the given warning as an error *)
+