Class virtual Definitions.visitor

class virtual visitor : cluster -> object .. end

method set_local : cluster -> unit

method do_local : cluster -> bool

method vadt : Lang.ADT.t -> unit

method vtype : Cil_types.logic_type_info -> unit

method vcomp : Cil_types.compinfo -> unit

method vicomp : Cil_types.compinfo -> unit

method vfield : Lang.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 vtypes : unit

Visit all typedefs

method vsymbols : unit

Visit all definitions

method vlemmas : unit

Visit all lemmas

method vself : unit

Visit all records, types, defs and lemmas

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 option -> unit

This local compinfo must be defined

method virtual on_icomp : Cil_types.compinfo -> (Lang.field * Lang.F.tau) list option -> unit

This local compinfo initialization 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