module type To_Use = sig
.. end
Computations of From can be done Functionwise (one result per function),
or Callwise (one result by call). The signature To_Use
is used to
describe the functions that are different between the two implementations.
val get_from_call : Cil_types.kernel_function -> Cil_types.stmt -> Function_Froms.t
How to find the Froms for a given call during the analysis.
val get_value_state : Cil_types.stmt -> Db.Value.state
How to find the state of Value at a given statement during the analysis.
val keep_base : Cil_types.kernel_function -> Base.t -> bool
Return true if the given base is in scope after a call to the given
function. (In particular, formals and locals of the function must result
in false
.)
val cleanup_and_save : Cil_types.kernel_function -> Function_Froms.t -> Function_Froms.t
Clean the given from (that have been computed for the given function),
optionally save them, and return the cleant result.