module type Values_To_Use_Sig = sig
.. end
Signature of the module explaining how to evaluatue some values during the
analysis. This is typically Db.Value, or a specialized versions of
Db.Value on more precise state.
val lval_to_zone_with_deps : Cil_types.stmt ->
deps:Locations.Zone.t option ->
for_writing:bool ->
Cil_types.lval -> Locations.Zone.t * Locations.Zone.t * bool
val expr_to_kernel_function : Cil_types.stmt ->
deps:Locations.Zone.t option ->
Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t
val get_stmt_state : Cil_types.stmt -> Db.Value.state
val access_expr : Cil_types.stmt -> Cil_types.exp -> Db.Value.t