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
typecallstack =
call_site list
Value callstacks, as used e.g. in Db.Value hooks
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 |
type
cacheable =
| |
Cacheable |
(* | Functions whose result can be safely cached | *) |
| |
NoCache |
(* | Functions whose result should not be cached, but for which the caller can still be cached. Typically, functions printing something during the analysis. | *) |
| |
NoCacheCallers |
(* | Functions for which neither the call, neither the callers, can be cached | *) |
type
call_result = {
|
c_values : |
|||
|
c_clobbered : |
(* | An over-approximation of the bases in which addresses of local variables might have been written | *) |
|
c_cacheable : |
(* | Is it possible to cache the result of this call? | *) |
|
c_from : |
(* | 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. | *) |
Results of a a call to a function
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