Frama-C:
Plug-ins:
Libraries:

Frama-C API - visitor

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 overridden further.

inherit Frama_c_kernel.Visitor.frama_c_inplace
method get_visit_error : unit -> exn option
  • returns

    a potential error during the visit of the AST (for instance a not_yet error while visiting assigns clause in behaviors).

method get_akind : unit -> E_ACSL.Analyses_types.annotation_kind
  • returns

    The current kind of annotation being visited.

method visit : 'a 'b. ?vcode_annot:bool -> ?vspec:bool -> (Frama_c_kernel.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 : Frama_c_kernel.Cil_types.file -> unit

visit file starts a visit of the AST from the given file node.

visit code_annot starts a visit of the AST from the given code_annot node.

visit_predicate p starts a visit of the AST from the given predicate node.