sig
val get_data_scope_at_stmt :
(Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval ->
Cil_datatype.Stmt.Hptset.t *
(Cil_datatype.Stmt.Hptset.t * Cil_datatype.Stmt.Hptset.t))
Pervasives.ref
val get_prop_scope_at_stmt :
(Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_datatype.Stmt.Hptset.t * Cil_types.code_annotation list)
Pervasives.ref
val check_asserts : (unit -> Cil_types.code_annotation list) Pervasives.ref
val rm_asserts : (unit -> unit) Pervasives.ref
val get_defs :
(Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval ->
(Cil_datatype.Stmt.Hptset.t * Locations.Zone.t option) option)
Pervasives.ref
val get_defs_with_type :
(Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval ->
((bool * bool) Cil_datatype.Stmt.Map.t * Locations.Zone.t option) option)
Pervasives.ref
type t_zones = Locations.Zone.t Cil_datatype.Stmt.Hashtbl.t
val build_zones :
(Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval -> Cil_datatype.Stmt.Hptset.t * Db.Scope.t_zones)
Pervasives.ref
val pretty_zones :
(Format.formatter -> Db.Scope.t_zones -> unit) Pervasives.ref
val get_zones :
(Db.Scope.t_zones -> Cil_types.stmt -> Locations.Zone.t) Pervasives.ref
end