module Visitor: sig
.. end
Frama-C visitors dealing with projects.
class type frama_c_visitor = object
.. end
Class type for a Db-aware visitor.
class frama_c_inplace :
frama_c_visitor
in-place visitor; always act in the current project.
class frama_c_copy : Project.t ->
frama_c_visitor
Copying visitor.
class frama_c_refresh : Project.t ->
frama_c_visitor
class generic_frama_c_visitor : Cil.visitor_behavior ->
frama_c_visitor
Generic class that abstracts over frama_c_inplace
and frama_c_copy
.
val visitFramacFileCopy : frama_c_visitor -> Cil_types.file -> Cil_types.file
Visit a file. This will re-cons all globals TWICE (so that it is
tail-recursive). Use
Cil.visitCilFileSameGlobals
if your visitor will
not change the list of globals.
val visitFramacFile : frama_c_visitor -> Cil_types.file -> unit
Same thing, but the result is ignored. The given visitor must thus be
an inplace visitor. Nothing is done if the visitor is a copy visitor.
val visitFramacFileSameGlobals : frama_c_visitor -> Cil_types.file -> unit
A visitor for the whole file that does not change the globals (but maybe
changes things inside the globals). Use this function instead of
Visitor.visitFramacFile
whenever appropriate because it is more
efficient for long files.
Consult the Plugin Development Guide for additional details.
val visitFramacGlobal : frama_c_visitor -> Cil_types.global -> Cil_types.global list
Visit a global.
val visitFramacKf : frama_c_visitor -> Kernel_function.t -> Kernel_function.t
Visit a kernel_function. More precisely, the entry point for the visit
will be the global corresponding to the last declaration/definition of
the kf. The returned kf is the one that has the varinfo
associated to the varinfo of the original kf. If this is a new kf, it is
however the responsibility of the visitor to insert it in the AST at
the appropriate place.
Since Aluminium-20160501
val visitFramacFunction : frama_c_visitor -> Cil_types.fundec -> Cil_types.fundec
val visitFramacExpr : frama_c_visitor -> Cil_types.exp -> Cil_types.exp
Visit an expression
val visitFramacLval : frama_c_visitor -> Cil_types.lval -> Cil_types.lval
Visit an lvalue
val visitFramacOffset : frama_c_visitor -> Cil_types.offset -> Cil_types.offset
Visit an lvalue or recursive offset
val visitFramacInitOffset : frama_c_visitor -> Cil_types.offset -> Cil_types.offset
Visit an initializer offset
val visitFramacInstr : frama_c_visitor -> Cil_types.instr -> Cil_types.instr list
Visit an instruction
val visitFramacStmt : frama_c_visitor -> Cil_types.stmt -> Cil_types.stmt
Visit a statement
val visitFramacBlock : frama_c_visitor -> Cil_types.block -> Cil_types.block
Visit a block
val visitFramacType : frama_c_visitor -> Cil_types.typ -> Cil_types.typ
Visit a type
val visitFramacVarDecl : frama_c_visitor -> Cil_types.varinfo -> Cil_types.varinfo
Visit a variable declaration
val visitFramacLogicVarDecl : frama_c_visitor -> Cil_types.logic_var -> Cil_types.logic_var
Visit a logic variable declaration
Since Magnesium-20151001
val visitFramacInit : frama_c_visitor ->
Cil_types.varinfo -> Cil_types.offset -> Cil_types.init -> Cil_types.init
Visit an initializer, pass also the global to which this belongs and the
offset.
val visitFramacAttributes : frama_c_visitor ->
Cil_types.attribute list -> Cil_types.attribute list
Visit a list of attributes
val visitFramacAnnotation : frama_c_visitor ->
Cil_types.global_annotation -> Cil_types.global_annotation
val visitFramacCodeAnnotation : frama_c_visitor ->
Cil_types.code_annotation -> Cil_types.code_annotation
val visitFramacAllocation : frama_c_visitor ->
Cil_types.identified_term Cil_types.allocation ->
Cil_types.identified_term Cil_types.allocation
val visitFramacAssigns : frama_c_visitor ->
Cil_types.identified_term Cil_types.assigns ->
Cil_types.identified_term Cil_types.assigns
val visitFramacFrom : frama_c_visitor ->
Cil_types.identified_term Cil_types.from ->
Cil_types.identified_term Cil_types.from
val visitFramacDeps : frama_c_visitor ->
Cil_types.identified_term Cil_types.deps ->
Cil_types.identified_term Cil_types.deps
val visitFramacFunspec : frama_c_visitor -> Cil_types.funspec -> Cil_types.funspec
val visitFramacLogicType : frama_c_visitor -> Cil_types.logic_type -> Cil_types.logic_type
val visitFramacPredicate : frama_c_visitor -> Cil_types.predicate -> Cil_types.predicate
val visitFramacPredicateNamed : frama_c_visitor ->
Cil_types.predicate Cil_types.named -> Cil_types.predicate Cil_types.named
val visitFramacIdPredicate : frama_c_visitor ->
Cil_types.identified_predicate -> Cil_types.identified_predicate
val visitFramacPredicates : frama_c_visitor ->
Cil_types.identified_predicate list -> Cil_types.identified_predicate list
val visitFramacIdTerm : frama_c_visitor ->
Cil_types.identified_term -> Cil_types.identified_term
visit identified_term.
Since Oxygen-20120901
val visitFramacTerm : frama_c_visitor -> Cil_types.term -> Cil_types.term
val visitFramacTermLval : frama_c_visitor -> Cil_types.term_lval -> Cil_types.term_lval
val visitFramacTermLhost : frama_c_visitor -> Cil_types.term_lhost -> Cil_types.term_lhost
val visitFramacTermOffset : frama_c_visitor -> Cil_types.term_offset -> Cil_types.term_offset
val visitFramacLogicInfo : frama_c_visitor -> Cil_types.logic_info -> Cil_types.logic_info
val visitFramacBehavior : frama_c_visitor -> Cil_types.funbehavior -> Cil_types.funbehavior
val visitFramacBehaviors : frama_c_visitor ->
Cil_types.funbehavior list -> Cil_types.funbehavior list
val visitFramacModelInfo : frama_c_visitor -> Cil_types.model_info -> Cil_types.model_info
val visitFramacExtended : frama_c_visitor ->
string * int * Cil_types.identified_predicate list ->
string * int * Cil_types.identified_predicate list