Class type Wp.Wpo.generator

class type generator = object .. end

method model : Wp.WpContext.model

Generate VCs for the given Property.

method compute_ip : Property.t -> t Bag.t

Generate VCs for call preconditions at the given statement.

method compute_call : Cil_types.stmt -> t Bag.t

Generate VCs for all functions matching provided behaviors and property names. For `~bhv` and `~prop` optional arguments, default and empty list means all properties.

method compute_main : ?fct:Wp.Wp_parameters.functions ->
?bhv:string list -> ?prop:string list -> unit -> t Bag.t