sig
module type Conversion =
sig
type extended_value
type internal_value
val extend_val :
Location_lift.Conversion.internal_value ->
Location_lift.Conversion.extended_value
val replace_val :
Location_lift.Conversion.internal_value ->
Location_lift.Conversion.extended_value ->
Location_lift.Conversion.extended_value
val restrict_val :
Location_lift.Conversion.extended_value ->
Location_lift.Conversion.internal_value
end
module Make :
functor
(Loc : Abstract_location.Internal) (Convert : sig
type extended_value
val extend_val :
Loc.value ->
extended_value
val replace_val :
Loc.value ->
extended_value ->
extended_value
val restrict_val :
extended_value ->
Loc.value
end) ->
sig
type value = Convert.extended_value
type location = Loc.location
type offset = Loc.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 partially_overlap : location -> location -> bool
val check_non_overlapping :
(Cil_types.lval * location) list ->
(Cil_types.lval * location) list -> unit Eval.evaluated
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 reduce_index_by_array_size :
size_expr:Cil_types.exp ->
index_expr:Cil_types.exp ->
Integer.t -> value -> value Eval.evaluated
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 reduce_loc_by_validity :
for_writing:bool ->
bitfield:bool ->
Cil_types.lval -> location -> location Eval.evaluated
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 Abstract_location.structure
end
end