module type S =sig
..end
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
Abstract_value.truth
for more details.val assume_no_overlap : partial:bool ->
location ->
location ->
(location * location)
Abstract_location.truth
partial
is true, the
concrete locations may be equal, but different locations must not overlap.
Otherwise, the locations must be completely separate.val assume_valid_location : for_writing:bool ->
bitfield:bool ->
location ->
location Abstract_location.truth
for_writing
boolean. Used to emit memory access alarms.
If the location is not completely valid, reduces it to its valid part.
bitfield
indicates whether the location may be the one of a bitfield;
if it is false, the location can be assumed to be byte aligned.val no_offset : offset
val forward_field : Cil_types.typ ->
Cil_types.fieldinfo ->
offset -> offset
val forward_index : Cil_types.typ ->
value ->
offset -> offset
forward_index typ value offset
computes the array index offset of
(Index (ind, off)), where the index expression ind
evaluates to value
and the remaining offset off
evaluates to offset
.
typ
must be the type pointed by the array.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
It must satisfy:
if B arg res
= v
then ∀ a ⊆ arg such that F a
⊆ res, a ⊆ v
i.e. B arg res
returns a value v
larger than all subvalues of arg
whose result through F is included in res
.
If F arg
∈ res
is impossible, then v
should be bottom.
Any n-ary operator may be considered as a unary operator on a vector
of values, the inclusion being lifted pointwise.
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