sig
type 'v truth = 'v Abstract_value.truth
module type S =
sig
type value
type location
type offset
val top : Abstract_location.S.location
val equal_loc :
Abstract_location.S.location -> Abstract_location.S.location -> bool
val equal_offset :
Abstract_location.S.offset -> Abstract_location.S.offset -> bool
val pretty_loc :
Stdlib.Format.formatter -> Abstract_location.S.location -> unit
val pretty_offset :
Stdlib.Format.formatter -> Abstract_location.S.offset -> unit
val to_value :
Abstract_location.S.location -> Abstract_location.S.value
val size : Abstract_location.S.location -> Int_Base.t
val assume_no_overlap :
partial:bool ->
Abstract_location.S.location ->
Abstract_location.S.location ->
(Abstract_location.S.location * Abstract_location.S.location)
Abstract_location.truth
val assume_valid_location :
for_writing:bool ->
bitfield:bool ->
Abstract_location.S.location ->
Abstract_location.S.location Abstract_location.truth
val no_offset : Abstract_location.S.offset
val forward_field :
Cil_types.typ ->
Cil_types.fieldinfo ->
Abstract_location.S.offset -> Abstract_location.S.offset
val forward_index :
Cil_types.typ ->
Abstract_location.S.value ->
Abstract_location.S.offset -> Abstract_location.S.offset
val forward_variable :
Cil_types.typ ->
Cil_types.varinfo ->
Abstract_location.S.offset ->
Abstract_location.S.location Eval.or_bottom
val forward_pointer :
Cil_types.typ ->
Abstract_location.S.value ->
Abstract_location.S.offset ->
Abstract_location.S.location Eval.or_bottom
val eval_varinfo : Cil_types.varinfo -> Abstract_location.S.location
val backward_variable :
Cil_types.varinfo ->
Abstract_location.S.location ->
Abstract_location.S.offset Eval.or_bottom
val backward_pointer :
Abstract_location.S.value ->
Abstract_location.S.offset ->
Abstract_location.S.location ->
(Abstract_location.S.value * Abstract_location.S.offset)
Eval.or_bottom
val backward_field :
Cil_types.typ ->
Cil_types.fieldinfo ->
Abstract_location.S.offset ->
Abstract_location.S.offset Eval.or_bottom
val backward_index :
Cil_types.typ ->
index:Abstract_location.S.value ->
remaining:Abstract_location.S.offset ->
Abstract_location.S.offset ->
(Abstract_location.S.value * Abstract_location.S.offset)
Eval.or_bottom
end
type 'loc key = 'loc Structure.Key_Location.key
module type Leaf =
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) truth
val assume_valid_location :
for_writing:bool -> bitfield:bool -> location -> 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 key : location Abstract_location.key
end
end