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