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: sig .. end
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?

*)
   c_from : (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.

*)
}

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