Class Definitions.visitorSource

Locality

method set_local : cluster -> unit
method do_local : cluster -> bool

Visiting items

method vadt : Wp__.Lang.ADT.t -> unit
method vcomp : Frama_c_kernel.Cil_types.compinfo -> unit
method vicomp : Frama_c_kernel.Cil_types.compinfo -> unit
method vfield : Wp__.Lang.Field.t -> unit
method vtau : Wp__.Lang.F.tau -> unit
method vparam : Wp__.Lang.F.var -> unit
method vterm : Wp__.Lang.F.term -> unit
method vpred : Wp__.Lang.F.pred -> unit
method vsymbol : Wp__.Lang.lfun -> unit
method vlemma : Wp__.LogicUsage.logic_lemma -> unit
method vcluster : cluster -> unit
method vlibrary : string -> unit
method vgoal : axioms option -> Wp__.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

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 : Frama_c_kernel.Cil_types.logic_type_info -> typedef -> unit

This local type must be defined

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

This local compinfo must be defined

method virtual on_icomp : Frama_c_kernel.Cil_types.compinfo -> (Wp__.Lang.field * Wp__.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