module Offsetmap_lattice_with_isotropy:sig
..end
Offsetmap.Make
type
numerical_widen_hint
typesize_widen_hint =
Integer.t
include Bounded_Join_Semi_Lattice
include With_Widening
include With_Cardinal_One
val pretty_typ : Cil_types.typ option -> t Pretty_utils.formatter
val is_isotropic : t -> bool
val topify_with_origin : Origin.t -> t -> t
Offsetmap_lattice_with_isotropy.is_isotropic
.val extract_bits : topify:Origin.kind ->
start:Integer.t -> stop:Integer.t -> size:Integer.t -> t -> bool * t
start
and stop
in the value of type t
,
assuming this value has size
bits. Return the corresponding value, and
a boolean indicating that an imprecision occurred during the operation.
In the latter case, the origin of the imprecision is flagged as having kind
topify
.val shift_bits : topify:Origin.kind -> offset:Integer.t -> size:Integer.t -> t -> t
size
, by offset
bits.
topify
indicates which operation caused this shift to take place,
for imprecision tracking.val merge_distinct_bits : topify:Origin.kind -> conflate_bottom:bool -> t -> t -> t
+
or |
are correct
implementations.)
The conflate_bottom
argument deals with bottom
values in either of the arguments. If conflate_bottom
holds, any
pre-existing bottom
value must result in bottom
. Otherwise,
the bottom
value is ignored.
topify
indicates which operation caused this merge to take place,
for imprecision tracking.
val merge_neutral_element : t
Offsetmap_lattice_with_isotropy.merge_distinct_bits
as the starting value.
This value must be neutral wrt. merging of values.val anisotropic_cast : size:Integer.t -> t -> t
size
bits. Returning the value argument
is alwas correct.