Module WpGenerator

module WpGenerator: sig .. end

class type computer = object .. end
val compute_ip : computer -> Property.t -> Wpo.t Bag.t
val compute_call : computer -> Cil_types.stmt -> Wpo.t Bag.t
val compute_kf : computer ->
?kf:Kernel_function.t ->
?bhv:string list -> ?prop:string list -> unit -> Wpo.t Bag.t
val compute_selection : computer ->
?fct:Wp_parameters.functions ->
?bhv:string list -> ?prop:string list -> unit -> Wpo.t Bag.t
val dumper : unit -> computer
val computer : Factory.setup -> Factory.driver -> computer