module Value_types:sig
..end
typecall_site =
Cil_types.kernel_function * Cil_types.kinstr
typecallstack =
call_site list
module Callsite:Datatype.S_with_collections
with type t = call_site
module Callstack:Datatype.S_with_collections
with type t = callstack
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?
| *) |
typelogic_dependencies =
Locations.Zone.t Cil_datatype.Logic_label.Map.t