diff --git a/src/plugins/wp/AssignsCompleteness.mli b/src/plugins/wp/AssignsCompleteness.mli index 04cd0c979670476142bd19a1124e3838e65051c0..8fa55bec1d546c61fddd6cdd9e6a7bc65c2ee968 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 92ebdc9eb289ebeca9ef6649dfa24b3b49076894..f4d84ab492ac2b2f55021f0cff8210752ab97293 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 \