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