Frama_c_kernel.Value_types
Declarations that are useful for plugins written on top of the results of Value.
type call_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
.
type callstack = 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 call_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.
type logic_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