module From:sig
..end
Functional dependencies between function inputs and function outputs.
exception Not_lval
exception raised by find_deps_no_transitivity_*
if the given expression
is not an lvalue.
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.
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
Not_lval
if the given expression is not a C lvalue.val self : State.t Stdlib.ref
val pretty : (Stdlib.Format.formatter -> Cil_types.kernel_function -> unit) Stdlib.ref
val display : (Stdlib.Format.formatter -> unit) Stdlib.ref
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
module Callwise:sig
..end