Wp.Definitions.cluster ->
object
  method do_local : Wp.Definitions.cluster -> bool
  method virtual on_cluster : Wp.Definitions.cluster -> unit
  method virtual on_comp :
    Cil_types.compinfo -> (Wp.Lang.field * Wp.Lang.F.tau) list -> unit
  method virtual on_dfun : Wp.Definitions.dfun -> unit
  method virtual on_dlemma : Wp.Definitions.dlemma -> unit
  method virtual on_library : string -> unit
  method virtual on_type :
    Cil_types.logic_type_info -> Wp.Definitions.typedef -> unit
  method virtual section : string -> unit
  method set_local : Wp.Definitions.cluster -> unit
  method vadt : Wp.Lang.ADT.t -> unit
  method vcluster : Wp.Definitions.cluster -> unit
  method vcomp : Cil_types.compinfo -> unit
  method vfield : Wp.Lang.Field.t -> unit
  method vgoal : Wp.Definitions.axioms option -> Wp.Lang.F.pred -> unit
  method vlemma : Wp.LogicUsage.logic_lemma -> unit
  method vlemmas : unit
  method vlibrary : string -> unit
  method vparam : Wp.Lang.F.var -> unit
  method vpred : Wp.Lang.F.pred -> unit
  method vself : unit
  method vsymbol : Wp.Lang.lfun -> unit
  method vsymbols : unit
  method vtau : Wp.Lang.F.tau -> unit
  method vterm : Wp.Lang.F.term -> unit
  method vtype : Cil_types.logic_type_info -> unit
  method vtypes : unit
end