sig
  class type computer =
    object
      method add_lemma : LogicUsage.logic_lemma -> unit
      method add_strategy : WpStrategy.strategy -> unit
      method compute : Wpo.t Bag.t
      method lemma : bool
      method model : Model.t
    end
  type functions =
      F_All
    | F_List of Cil_datatype.Kf.Set.t
    | F_Skip of Cil_datatype.Kf.Set.t
  val compute_ip : Generator.computer -> Property.t -> Wpo.t Bag.t
  val compute_call : Generator.computer -> Cil_types.stmt -> Wpo.t Bag.t
  val compute_kf :
    Generator.computer ->
    ?kf:Kernel_function.t ->
    ?bhv:string list -> ?prop:string list -> unit -> Wpo.t Bag.t
  val compute_selection :
    Generator.computer ->
    ?fct:Generator.functions ->
    ?bhv:string list -> ?prop:string list -> unit -> Wpo.t Bag.t
end