Frama-C API - visitor
Locality
method set_local : cluster -> unit
method do_local : cluster -> bool
Visiting items
method vtype : Frama_c_kernel.Cil_types.logic_type_info -> unit
method vcomp : Frama_c_kernel.Cil_types.compinfo -> unit
method vicomp : Frama_c_kernel.Cil_types.compinfo -> unit
method vcluster : cluster -> unit
method vgoal : axioms option -> Wp__.Lang.F.pred -> unit
Visited definitions
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