From 038652763431e7b3b49b158bcea1e32d5326a3a3 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 7 Oct 2020 11:16:32 +0200
Subject: [PATCH] [wp] export pedantic-assigns key
---
src/plugins/wp/AssignsCompleteness.mli | 2 ++
src/plugins/wp/Makefile.in | 2 +-
2 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/AssignsCompleteness.mli b/src/plugins/wp/AssignsCompleteness.mli
index 04cd0c97967..8fa55bec1d5 100644
--- a/src/plugins/wp/AssignsCompleteness.mli
+++ b/src/plugins/wp/AssignsCompleteness.mli
@@ -34,3 +34,5 @@ val is_complete: Kernel_function.t -> bool
val warn: Kernel_function.t -> unit
(** Displays a warning if the given kernel function has incomplete assigns.
Note that the warning is configured with [~once] set to [true]. *)
+
+val wkey_pedantic: Wp_parameters.warn_category
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 92ebdc9eb28..f4d84ab492a 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -234,7 +234,7 @@ WP_API_BASE= \
LogicUsage.mli RefUsage.mli \
normAtLabels.mli \
wpPropId.mli mcfg.ml \
- Context.mli Warning.mli wpContext.mli \
+ Context.mli Warning.mli AssignsCompleteness.mli wpContext.mli \
Lang.mli Repr.mli Passive.mli Splitter.mli \
LogicBuiltins.mli Definitions.mli \
Cint.mli Cfloat.mli Vset.mli Cstring.mli \
--
GitLab