Module Value_types

module Value_types: sig .. end
Declarations that are useful for plugins written on top of the results of Value.

type call_site = Cil_types.kernel_function * Cil_types.kinstr 
type callstack = 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: Datatype.S_with_collections  with type t = callstack
type 'a callback_result = 
| Normal of 'a
| NormalStore of 'a * int
| Reuse of int
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 : (Cvalue.V_Offsetmap.t option * Cvalue.Model.t) list;
   c_clobbered : Base.SetLattice.t; (*An over-approximation of the bases in which addresses of local variables might have been written*)
   c_cacheable : cacheable; (*Is it possible to cache the result of this call?*)
}
Results of a a call to a function
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