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