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.F.ADT.t -> unit   method vcluster : Wp.Definitions.cluster -> unit   method vcomp : Cil_types.compinfo -> unit   method vfield : Wp.Lang.F.Field.t -> unit   method vgoal : Wp.Definitions.axioms option -> Wp.Lang.F.pred -> unit   method vlemma : Wp.LogicUsage.logic_lemma -> 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 vtau : Wp.Lang.F.tau -> unit   method vterm : Wp.Lang.F.term -> unit   method vtype : Cil_types.logic_type_info -> unit end