Module WpRTE

module WpRTE: sig .. end
Invoke RTE to generate missing annotations for the given function and model.

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