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

Value call-site. A callsite (f,p) represents a call at function f invoked from program point p.

type callstack = call_site list

Value callstacks, as used e.g. in Db.Value hooks.

The head call site (f,p) is the most recent one, where current function f has been called from program point p.

Therefore, the tail call site is expected to be (main,Kglobal) where main is the global entry point.

Moreover, given two consecutive call-sites …(_,p);(g,_)… in a callstack, program point p is then expected to live in function g.

module Callsite: Datatype.S_with_collections  with type t = call_site

module Callstack: sig .. end

type 'a callback_result =

type call_froms = (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.

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