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