sig
module type Data =
sig
type t
val equal : Layout.Data.t -> Layout.Data.t -> bool
val compare : Layout.Data.t -> Layout.Data.t -> int
val pretty : Layout.Data.t Pretty_utils.formatter
end
type offset = Field of Cil_types.fieldinfo | Index of Cil_types.typ * int
type lvalue =
Eval of Cil_types.exp
| Tval of Cil_types.term
| Assigned of Cil_types.stmt
module Offset :
sig
type t = offset
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : t Pretty_utils.formatter
val index : Cil_types.typ -> Layout.offset
val field : Cil_types.fieldinfo -> Layout.offset
val typeof : Layout.offset -> Cil_types.typ
val typeof_chain : Cil_types.typ -> Layout.offset list -> Cil_types.typ
val pp_chain :
Cil_types.typ -> Layout.offset list Pretty_utils.formatter
type cache
val cache : unit -> Layout.Offset.cache
val field_offset :
Layout.Offset.cache -> Cil_types.fieldinfo -> int * int
val range : Layout.Offset.cache -> Layout.offset -> (int * int) * int
val sizeof : Layout.offset -> int
end
module Lvalue :
sig
type t = lvalue
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : t Pretty_utils.formatter
end
type alias = NotUsed | NotAliased | Aliased
type usage = Value | Deref | Array
type deref = Layout.usage * Cil_types.typ
module Alias :
sig
val use : Layout.alias -> Layout.alias
val merge : Layout.alias -> Layout.alias -> Layout.alias
val alias : Layout.alias -> Layout.alias -> Layout.alias
val is_aliased : Layout.alias -> bool
val pretty : Layout.alias Pretty_utils.formatter
end
module Usage :
sig
val pretty : Layout.usage Pretty_utils.formatter
val merge : Layout.usage -> Layout.usage -> Layout.usage
val is_shifted : Layout.usage -> bool
val is_aliased : Layout.usage -> bool
end
module Deref :
sig
type t = deref
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : t Pretty_utils.formatter
end
type 'a value =
Int of Ctypes.c_int
| Float of Ctypes.c_float
| Pointer of 'a
module Value :
sig
val compare :
('a -> 'a -> int) -> 'a Layout.value -> 'a Layout.value -> int
val equal :
('a -> 'a -> bool) -> 'a Layout.value -> 'a Layout.value -> bool
val pretty :
'a Pretty_utils.formatter -> 'a Layout.value Pretty_utils.formatter
val sizeof : 'a Layout.value -> int
val pointed : 'a Layout.value -> 'a option
val merge :
('a -> 'a -> 'a) ->
'a Layout.value -> 'a Layout.value -> 'a Layout.value option
end
module Matrix :
sig
val gcd : int -> int -> int
val pretty : int list Pretty_utils.formatter
val sizeof : int -> int list -> int
val merge : int list -> int list -> int list
end
type dim = Raw of int | Dim of int * int list
type 'a range = private {
ofs : int;
len : int;
reg : 'a;
dim : Layout.dim;
}
type 'a overlay = 'a Layout.range list
type 'a merger = raw:bool -> 'a -> 'a -> 'a
module Range :
sig
val pretty :
'a Pretty_utils.formatter -> 'a Layout.range Pretty_utils.formatter
val overlap :
'a Pretty_utils.formatter ->
'a Layout.merger ->
'a Layout.range -> 'a Layout.range -> 'a Layout.range
val included : int -> int -> 'a Layout.range -> bool
end
module Overlay :
sig
val pretty :
?title:(Format.formatter -> unit) ->
'a Pretty_utils.formatter -> 'a Layout.overlay Pretty_utils.formatter
val merge :
'a Pretty_utils.formatter ->
'a Layout.merger ->
'a Layout.overlay -> 'a Layout.overlay -> 'a Layout.overlay
val once : 'a -> 'a Layout.overlay -> bool
end
type 'a layout = { sizeof : int; layout : 'a Layout.overlay; }
module Compound :
sig
val garbled :
Layout.Offset.cache -> Layout.offset -> 'a -> 'a Layout.layout
val reshape :
eq:('a -> 'a -> bool) ->
flat:bool -> pack:bool -> 'a Layout.layout -> 'a Layout.layout
end
type 'a cluster =
Empty
| Garbled
| Chunk of 'a Layout.value
| Layout of 'a Layout.layout
module Cluster :
sig
val pretty :
'a Pretty_utils.formatter -> 'a Layout.cluster Pretty_utils.formatter
val deref : pointed:'a Lazy.t -> Layout.deref -> 'a Layout.cluster
val shift :
Layout.Offset.cache ->
'a Pretty_utils.formatter ->
Layout.offset ->
'a -> inline:bool -> 'a Layout.cluster -> 'a Layout.layout
val merge :
'a Pretty_utils.formatter ->
'a Layout.merger ->
'a Layout.cluster -> 'a Layout.cluster -> 'a Layout.cluster
val is_empty : 'a Layout.cluster -> bool
val is_garbled : 'a Layout.cluster -> bool
val reshape :
eq:('a -> 'a -> bool) ->
flat:bool -> pack:bool -> 'a Layout.cluster -> 'a Layout.cluster
end
type 'a from =
Fvar of Cil_types.varinfo
| Ffield of 'a * int
| Findex of 'a
| Fderef of 'a
| Farray of 'a
type root =
Rnone
| Rfield of Cil_types.varinfo * int
| Rindex of Cil_types.varinfo
| Rtop
module Root :
sig
val pretty : Layout.root Pretty_utils.formatter
val from : root:('a -> Layout.root) -> 'a Layout.from -> Layout.root
val merge : Layout.root -> Layout.root -> Layout.root
val indexed : Layout.root -> bool
val framed : Layout.root -> bool
end
type chunks = Qed.Intset.t
type 'a chunk =
Mref of 'a
| Mmem of Layout.root * 'a Layout.value
| Mraw of Layout.root * 'a option
| Mcomp of Layout.chunks * 'a Layout.overlay
module Chunk :
sig
val empty : Layout.chunks
val singleton : int -> Layout.chunks
val union : Layout.chunks -> Layout.chunks -> Layout.chunks
val disjoint : Layout.chunks -> Layout.chunks -> bool
val union_map : ('a -> Layout.chunks) -> 'a list -> Layout.chunks
val mem : int -> Layout.chunks -> bool
val pretty :
int Pretty_utils.formatter -> Layout.chunks Pretty_utils.formatter
end
module RW :
sig val default : unit -> bool val merge : bool -> bool -> bool end
module Flat :
sig val default : unit -> bool val merge : bool -> bool -> bool end
module Pack :
sig val default : unit -> bool val merge : bool -> bool -> bool end
end