Frama-C API - WpRTE
val generate : WpContext.model -> Frama_c_kernel.Kernel_function.t -> unit
Invoke RTE to generate missing annotations for the given function and model.
val generate_all : WpContext.model -> unit
Invoke RTE on all selected functions
val missing_guards : WpContext.model -> Frama_c_kernel.Kernel_function.t -> bool
Returns true
if RTE annotations should be generated for the given function and model (and are not generated yet).