module Value_types:sig
..end
Declarations that are useful for plugins written on top of the results of Value.
typecall_site =
Cil_types.kernel_function * Cil_types.kinstr
Value call-site.
A callsite (f,p)
represents a call at function f
invoked
from program point p
.
typecallstack =
call_site list
Value callstacks, as used e.g. in Db.Value hooks.
The head call site (f,p)
is the most recent one,
where current function f
has been called from program point p
.
Therefore, the tail call site is expected to be (main,Kglobal)
where main
is the global entry point.
Moreover, given two consecutive call-sites …(_,p);(g,_)…
in a callstack,
program point p
is then expected to live in function g
.
module Callsite:Datatype.S_with_collections
with type t = call_site
module Callstack:sig
..end
type 'a
callback_result =
| |
Normal of |
| |
NormalStore of |
| |
Reuse of |
typecall_froms =
(Function_Froms.froms * Locations.Zone.t) option
If not None, the froms of the function, and its sure outputs; i.e. the dependencies of the result, and the dependencies of each zone written to.
typelogic_dependencies =
Locations.Zone.t Cil_datatype.Logic_label.Map.t
Dependencies for the evaluation of a term or a predicate: for each program point involved, sets of zones that must be read