Frama-C API - `Register`

Interface for the occurrence plugin.

val self : Frama_c_kernel.State.t

val get_last_result : unit -> ((Frama_c_kernel.Cil_types.kernel_function option * Frama_c_kernel.Cil_types.kinstr * Frama_c_kernel.Cil_types.lval) list * Frama_c_kernel.Cil_types.varinfo) option

val get : Frama_c_kernel.Cil_types.varinfo -> (Frama_c_kernel.Cil_types.kernel_function option * Frama_c_kernel.Cil_types.kinstr * Frama_c_kernel.Cil_types.lval) list

Return the occurrences of the given varinfo. An occurrence ki, lv is a left-value lv which uses the location of vi at the position ki.

val print_all : unit -> unit

Print all the occurrence of each variable declarations.

type access_type =

| Read
| Write
| Both

val classify_accesses : (Frama_c_kernel.Cil_types.kernel_function option * Frama_c_kernel.Cil_types.kinstr * Frama_c_kernel.Cil_types.lval) -> access_type

Frama-C API - Register

Frama-C API - `Register`