Db.From
Functional dependencies between function inputs and function outputs.
exception raised by find_deps_no_transitivity_*
if the given expression is not an lvalue.
val find_deps_no_transitivity :
( Cil_types.stmt -> Cil_types.exp -> Locations.Zone.t ) Stdlib.ref
val find_deps_no_transitivity_state :
( Cvalue.Model.t -> Cil_types.exp -> Locations.Zone.t ) Stdlib.ref
val find_deps_term_no_transitivity_state :
( Cvalue.Model.t ->
Cil_types.term ->
Value_types.logic_dependencies )
Stdlib.ref