sig
module Defs :
sig
val get_defs :
Kernel_function.t ->
Cil_types.stmt ->
Cil_types.lval ->
(Cil_datatype.Stmt.Hptset.t * Locations.Zone.t option) option
val get_defs_with_type :
Kernel_function.t ->
Cil_types.stmt ->
Cil_types.lval ->
((bool * bool) Cil_datatype.Stmt.Map.t * Locations.Zone.t option)
option
end
module Datascope :
sig
val get_data_scope_at_stmt :
Kernel_function.t ->
Cil_types.stmt ->
Cil_types.lval ->
Cil_datatype.Stmt.Hptset.t *
(Cil_datatype.Stmt.Hptset.t * Cil_datatype.Stmt.Hptset.t)
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
val check_asserts : unit -> Cil_types.code_annotation list
val rm_asserts : unit -> unit
end
module Zones :
sig
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 * Scope.Zones.t_zones
val pretty_zones : Format.formatter -> Scope.Zones.t_zones -> unit
val get_zones :
Scope.Zones.t_zones -> Cil_types.stmt -> Locations.Zone.t
end
end