Module CfgWP

module CfgWP: sig .. end

module WpLog: Wp_parameters
module VC: 
functor (M : Memory.Model) -> sig .. end
val add_qed_check : Wpo.t Bag.t Pervasives.ref ->
Model.t -> qed:Lang.F.t -> raw:Lang.F.t -> goal:Lang.F.pred -> unit
module Computer: 
functor (M : Memory.Model) -> sig .. end