module type S =sig
..end
type
value
type
location
type
offset
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 offset_cardinal_zero_or_one : offset -> bool
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 reduce_index_by_array_size : size_expr:Cil_types.exp ->
index_expr:Cil_types.exp ->
Integer.t ->
value -> value Eval.evaluated
reduce_index_by_array_size ~size_expr ~index_expr size index
reduces
the value index
to fit into the interval 0..(size-1)
. It also returns
out-of-bound alarms if it was not already the case. size_expr
and
index_expr
are the Cil expressions of the array size and the index,
needed to create the alarms.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
reduce_loc_by_validity for_writing bitfield lval loc
reduce the location
loc
by its valid part for a read or write operation, according to the
for_writing
boolean. It also returns the alarms ensuring this validity.
bitfield
indicates whether the location may be the one of a bitfield;
if it does not hold, the location is assumed to be byte aligned.
lval
is only used to create the alarms.
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