Definitions.visitor
method set_local : cluster -> unit
method do_local : cluster -> bool
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
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