Module Db.From

module From: sig .. end

Functional dependencies between function inputs and function outputs.

See also internal documentation.

exception Not_lval

exception raised by find_deps_no_transitivity_* if the given expression is not an lvalue.

Since Aluminium-20160501

val compute_all : (unit -> unit) Stdlib.ref

val compute_all_calldeps : (unit -> unit) Stdlib.ref

val compute : (Cil_types.kernel_function -> unit) Stdlib.ref

val is_computed : (Cil_types.kernel_function -> bool) Stdlib.ref

Check whether the from analysis has been performed for the given function.

Returns true iff the analysis has been performed

val get : (Cil_types.kernel_function -> Function_Froms.t) Stdlib.ref

val access : (Locations.Zone.t -> Function_Froms.Memory.t -> Locations.Zone.t) Stdlib.ref

val find_deps_no_transitivity : (Cil_types.stmt -> Cil_types.exp -> Locations.Zone.t) Stdlib.ref

val find_deps_no_transitivity_state : (Db.Value.state -> Cil_types.exp -> Locations.Zone.t) Stdlib.ref

val find_deps_term_no_transitivity_state : (Db.Value.state -> Cil_types.term -> Value_types.logic_dependencies)
       Stdlib.ref

Raises Not_lval if the given expression is not a C lvalue.

val self : State.t Stdlib.ref

Pretty printing

val pretty : (Stdlib.Format.formatter -> Cil_types.kernel_function -> unit) Stdlib.ref

val display : (Stdlib.Format.formatter -> unit) Stdlib.ref

Callback

module Record_From_Callbacks: Hook.Iter_hook  with type param =
                          Kernel_function.t Stack.t *
                          Function_Froms.Memory.t Stmt.Hashtbl.t *
                          (Kernel_function.t * Function_Froms.Memory.t) list
                            Stmt.Hashtbl.t

Access to callwise-stored data

module Callwise: sig .. end