sig
type value
type location
type offset
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 : Format.formatter -> Abstract_location.S.location -> unit
val pretty_offset : 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 partially_overlap :
Abstract_location.S.location -> Abstract_location.S.location -> bool
val check_non_overlapping :
(Cil_types.lval * Abstract_location.S.location) list ->
(Cil_types.lval * Abstract_location.S.location) list ->
unit Eval.evaluated
val offset_cardinal_zero_or_one : Abstract_location.S.offset -> bool
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 reduce_index_by_array_size :
size_expr:Cil_types.exp ->
index_expr:Cil_types.exp ->
Integer.t ->
Abstract_location.S.value -> Abstract_location.S.value Eval.evaluated
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 reduce_loc_by_validity :
for_writing:bool ->
bitfield:bool ->
Cil_types.lval ->
Abstract_location.S.location ->
Abstract_location.S.location Eval.evaluated
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