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