Class `Visitor.frama_c_copy`

Copying visitor. The Project.t argument specifies in which project the visitor creates the new values. (Technically, the method fill_global_tables is called inside this project.) See File.init_project_from_visitor and create_project_from_visitor for possible uses.

inherit Frama_c_kernel.Cil.cilVisitor

method frama_c_plain_copy : frama_c_visitor

same as plain_copy_visitor but for frama-c specific methods

method vstmt_aux : Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.stmt Frama_c_kernel.Cil.visitAction

Replacement of vstmt.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

method vglob_aux : Frama_c_kernel.Cil_types.global ->
  Frama_c_kernel.Cil_types.global list Frama_c_kernel.Cil.visitAction

Replacement of vglob.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

method current_kf : Frama_c_kernel.Cil_types.kernel_function option

link to the kernel function currently being visited. NB: for copy visitors, the link is to the original kf (anyway, the new kf is created only after the visit is over).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

method set_current_kf : Frama_c_kernel.Cil_types.kernel_function -> unit

Internal use only.

method reset_current_kf : unit -> unit

Internal use only.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c.kernel/Frama_c_kernel/Visitor/class-frama_c_copy/index.html

Class `Visitor.frama_c_copy`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c.kernel/Frama_c_kernel/Visitor/class-frama_c_copy/index.html

Class Visitor.frama_c_copy

Class `Visitor.frama_c_copy`