Module type Abstract_location.S

module type S = sig .. end
Signature of abstract memory locations.

type value 
type location 
abstract locations
type offset 
abstract offsets
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
Needed for unspecified sequences.
val offset_cardinal_zero_or_one : offset -> bool
Needed for Evaluation.get_influential_vars

Forward Offset Operations


val no_offset : offset
val forward_field : Cil_types.typ ->
Cil_types.fieldinfo ->
offset -> offset
Computes the field offset of a fieldinfo, with the given remaining offset. The given type must the one of the structure or the union.
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.

Forward Locations Operations



Evaluation of the location of an lvalue, when the offset has already been evaluated. In case of a pointer, its expression has also been evaluated to a value.
val forward_variable : Cil_types.typ ->
Cil_types.varinfo ->
offset -> location Eval.or_bottom
Var case in the AST: the host is a variable.
val forward_pointer : Cil_types.typ ->
value ->
offset -> location Eval.or_bottom
Mem case in the AST: the host is a pointer.
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.

Backward Operations



For an unary forward operation F, the inverse backward operator B tries to reduce the argument values of the operation, given its result.

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 argres 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