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