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