Module WpRTE

module WpRTE: sig .. end

Returns 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

Invoke RTE to generate missing annotations for the given function and model.

val missing_guards : Kernel_function.t -> Model.t -> bool

Returns true if RTE annotations should be generated for the given function and model (and are not generated yet).