Module Register

module Register: sig .. end

Register the plugin in the Frama-C kernel.


val self : State.t
val get_last_result : unit ->
((Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.lval) list *
Cil_types.varinfo)
option
val get : Cil_types.varinfo ->
(Cil_types.kernel_function option * Cil_types.kinstr * 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 : Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.lval ->
access_type

Occurrence has found the given lv somewhere inside ki. We try to find whether this was inside a read or a write operation. This is difficult to do directly inside the occurrence class, as the vlval method has no information about the origin of the lval it was called on