Value_types (frama-c.Frama_c_kernel.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 =

| Normal of 'a

| NormalStore of 'a * int

| Reuse of int

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