sig
  val compute :
    Cil2cfg.t ->
    WpStrategy.strategy ->
    VC.t_prop list * (Format.formatter -> Cil2cfg.edge -> unit)
end