sig
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 :
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 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
type 'a key = 'a Structure.Key_Location.k
type 'a structure = 'a Structure.Key_Location.structure
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 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
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 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 mem : 'a key -> bool
val get : 'a key -> (location -> 'a) option
val set : 'a key -> 'a -> location -> location
end
end