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 |
| |
NoCache |
| |
NoCacheCallers |
type
call_result = {
|
c_values : (Cvalue.V_Offsetmap.t option * Cvalue.Model.t) list ; |
|
c_clobbered : Base.SetLattice.t ; |
|
c_cacheable : cacheable ; |
}
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