sig
type 'a key = 'a Structure.Key_Location.key
val create_key : string -> 'a key
val eq_type : 'a key -> 'b key -> ('a, 'b) Structure.eq option
val print : 'a key Pretty_utils.formatter
val compare : 'a key -> 'b key -> int
val equal : 'a key -> 'b key -> bool
val hash : 'a key -> int
val tag : 'a key -> int
type 'a data = (module Abstract_location.S with type location = 'a)
type 'a structure =
Unit : unit structure
| Leaf : 'a key * 'a data -> 'a structure
| Node : 'a structure * 'b structure -> ('a * 'b) structure
val eq_structure :
'a structure -> 'b structure -> ('a, 'b) Structure.eq option
module type Internal =
sig
type value
type location
type offset
val top : location
val equal_loc : location -> location -> bool
val equal_offset : offset -> offset -> bool
val pretty_loc : Format.formatter -> location -> unit
val pretty_offset : Format.formatter -> offset -> unit
val to_value : location -> value
val size : location -> Int_Base.t
val assume_no_overlap :
partial:bool ->
location -> location -> (location * location) Abstract_location.truth
val assume_valid_location :
for_writing:bool ->
bitfield:bool -> location -> location Abstract_location.truth
val no_offset : offset
val forward_field :
Cil_types.typ -> Cil_types.fieldinfo -> offset -> offset
val forward_index : Cil_types.typ -> value -> offset -> offset
val forward_variable :
Cil_types.typ ->
Cil_types.varinfo -> offset -> location Eval.or_bottom
val forward_pointer :
Cil_types.typ -> value -> offset -> location Eval.or_bottom
val eval_varinfo : Cil_types.varinfo -> location
val backward_variable :
Cil_types.varinfo -> location -> offset Eval.or_bottom
val backward_pointer :
value -> offset -> location -> (value * offset) Eval.or_bottom
val backward_field :
Cil_types.typ ->
Cil_types.fieldinfo -> offset -> offset Eval.or_bottom
val backward_index :
Cil_types.typ ->
index:value ->
remaining:offset -> offset -> (value * offset) Eval.or_bottom
val structure : location structure
end
module type External =
sig
type value
type location
type offset
val top : location
val equal_loc : location -> location -> bool
val equal_offset : offset -> offset -> bool
val pretty_loc : Format.formatter -> location -> unit
val pretty_offset : Format.formatter -> offset -> unit
val to_value : location -> value
val size : location -> Int_Base.t
val assume_no_overlap :
partial:bool ->
location -> location -> (location * location) Abstract_location.truth
val assume_valid_location :
for_writing:bool ->
bitfield:bool -> location -> location Abstract_location.truth
val no_offset : offset
val forward_field :
Cil_types.typ -> Cil_types.fieldinfo -> offset -> offset
val forward_index : Cil_types.typ -> value -> offset -> offset
val forward_variable :
Cil_types.typ ->
Cil_types.varinfo -> offset -> location Eval.or_bottom
val forward_pointer :
Cil_types.typ -> value -> offset -> location Eval.or_bottom
val eval_varinfo : Cil_types.varinfo -> location
val backward_variable :
Cil_types.varinfo -> location -> offset Eval.or_bottom
val backward_pointer :
value -> offset -> location -> (value * offset) Eval.or_bottom
val backward_field :
Cil_types.typ ->
Cil_types.fieldinfo -> offset -> offset Eval.or_bottom
val backward_index :
Cil_types.typ ->
index:value ->
remaining:offset -> offset -> (value * offset) Eval.or_bottom
val structure : location structure
val mem : 'a key -> bool
val get : 'a key -> (location -> 'a) option
val set : 'a key -> 'a -> location -> location
end
end