module WpRTE:sig
..end
true
is call pre-conditions have been already
generated by RTE.val is_precond_generated : Kernel_function.t -> bool
val generate : Kernel_function.t -> Model.t -> unit
val missing_guards : Kernel_function.t -> Model.t -> bool
true
if RTE annotations should be generated for
the given function and model (and are not generated yet).