module WpRTE:sig
..end
val generate : WpContext.model -> Kernel_function.t -> unit
val missing_guards : WpContext.model -> Kernel_function.t -> bool
true
if RTE annotations should be generated for
the given function and model (and are not generated yet).