class virtual visitor : cluster ->
object
.. end
Locality
method set_local : cluster -> unit
method do_local : cluster -> bool
Visiting items
method vadt : Lang.F.ADT.t -> unit
method vtype : Cil_types.logic_type_info -> unit
method vcomp : Cil_types.compinfo -> unit
method vfield : Lang.F.Field.t -> unit
method vtau : Lang.F.tau -> unit
method vparam : Lang.F.var -> unit
method vterm : Lang.F.term -> unit
method vpred : Lang.F.pred -> unit
method vsymbol : Lang.lfun -> unit
method vlemma : LogicUsage.logic_lemma -> unit
method vcluster : cluster -> unit
method vlibrary : string -> unit
method vgoal : axioms option -> Lang.F.pred -> unit
method vself : unit
Visited definitions
method virtual section : string -> unit
Comment
method virtual on_library : string -> unit
External library to import
method virtual on_cluster : cluster -> unit
Outer cluster to import
method virtual on_type : Cil_types.logic_type_info -> typedef -> unit
This local type must be defined
method virtual on_comp : Cil_types.compinfo -> (Lang.field * Lang.F.tau) list -> unit
This local compinfo must be defined
method virtual on_dlemma : dlemma -> unit
This local lemma must be defined
method virtual on_dfun : dfun -> unit
This local function must be defined