object
  method compute_call : Cil_types.stmt -> Wp.Wpo.t Bag.t
  method compute_ip : Property.t -> Wp.Wpo.t Bag.t
  method compute_main :
    ?fct:Wp.Wp_parameters.functions ->
    ?bhv:string list -> ?prop:string list -> unit -> Wp.Wpo.t Bag.t
  method model : Wp.WpContext.model
end