class visitor :Options.category ->
object
..end
Visitor to visit the AST in the same manner than the injector.
new visitor cat
creates a visitor with cat
as the category to use for
the Error
module in the visitor.
For the root of the AST, not the global level, only visit the cases that
are relevant to E-ACSL. Each case is handled by a method of the visitor. The
cases are similar, and similarly named as the ones of the function
case_globals
.
For the rest of the AST, the kind of the visited annotation is recorded and
accessed through the method get_akind
. While visiting annotations
currently not supported by E-ACSL, the get_visit_error
returns a not_yet
exception. Any visitor that inherits from E_acsl_visitor.visitor
can
decide wether continue its processing or not as it sees fit.
As a result of the custom visit of the AST, the methods vcode_annot
and
vspec
skip their children, since they are already visited by vstmt_aux
.
Be sure to use the method visit
(and associated methods) if you need to
visit the children of those nodes.
To support these functionalities, the methods vglob_aux
and vstmt_aux
have been heavily modified and should not be overriden further.
method private default : unit -> Cil_types.global list Cil.visitAction
method builtin : Cil_types.varinfo -> Cil_types.global list Cil.visitAction
method fc_compiler_builtin : Cil_types.varinfo -> Cil_types.global list Cil.visitAction
method rtl_symbol : Cil_types.global -> Cil_types.global list Cil.visitAction
method fc_stdlib_generated : Cil_types.varinfo -> Cil_types.global list Cil.visitAction
method var_fun_decl : Cil_types.varinfo -> Cil_types.global list Cil.visitAction
method var_init : Cil_types.varinfo -> Cil_types.global list Cil.visitAction
method var_def : Cil_types.varinfo -> Cil_types.init -> Cil_types.global list Cil.visitAction
method glob_annot : Cil_types.global_annotation -> Cil_types.global list Cil.visitAction
method fun_def : Cil_types.fundec -> Cil_types.global list Cil.visitAction
method get_visit_error : unit -> exn option
not_yet
error while visiting assigns clause in behaviors).
the current visit error.method get_akind : unit -> Analyses_types.annotation_kind
method visit : 'a 'b.
?vcode_annot:bool ->
?vspec:bool -> (Visitor.frama_c_visitor -> 'a -> 'b) -> 'a -> 'b
visit ?vode_annot ?vspec visit_func item
starts a visit of the AST
from item
with the Frama-C visit function visit_func
.
If vcode_annot
is true, then the method vcode_annot
will visit its
children, otherwise they are skipped and will only be visited through
vstmt_aux
.
If vspec
is true, then the method vspec
will visit its children,
otherwise they are skipped and will only be visited through
vstmt_aux
.
method visit_file : Cil_types.file -> unit
visit file
starts a visit of the AST from the given file
node.
see documentation in e_acsl_visitor.mli
method visit_code_annot : Cil_types.code_annotation -> Cil_types.code_annotation
visit code_annot
starts a visit of the AST from the given code_annot
node.
see documentation in e_acsl_visitor.mli
method visit_predicate : Cil_types.predicate -> Cil_types.predicate
visit_predicate p
starts a visit of the AST from the given predicate
node.
see documentation in e_acsl_visitor.mli