sig val generate : WpContext.model -> Kernel_function.t -> unit val missing_guards : WpContext.model -> Kernel_function.t -> bool end