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 =

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