Parameter Make.V

include Lattice_type.Bounded_Join_Semi_Lattice
include Lattice_type.Join_Semi_Lattice

datatype of element of the lattice

include Datatype.S
include Datatype.S_no_copy
include Datatype.Ty
type t
val ty : t Type.t
val name : string

Unique name of the datatype.

val descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val pretty : Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

val mem_project : (Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

val join : t -> t -> t

over-approximation of union

val is_included : t -> t -> bool

is first argument included in the second?

val bottom : t

smallest element

include Lattice_type.With_Cardinal_One with type t := t
val cardinal_zero_or_one : t -> bool
type widen_hint

Hints for the widening.

val widen : ?size:Integer.t -> ?hint:widen_hint -> t -> t -> t

widen ~size ~hint v1 v2 is an over-approximation of join v1 v2. size is the size (in bits) of the widened value, and hint is some hint for the widening.

val pretty_typ : Cil_types.typ option -> t Pretty_utils.formatter

Isotropy

val is_isotropic : t -> bool

Are the bits independent?

val topify_with_origin : Origin.t -> t -> t

Force a value to be isotropic, when a loss of imprecision occurs. The resulting value must verify is_isotropic.

Reading bits of values

val extract_bits : topify:Origin.kind -> start:Integer.t -> stop:Integer.t -> size:Integer.t -> t -> bool * t

Extract the bits between 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

Left-shift the given value, of size 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

Merge the bits of the two given values, that span disjoint bit ranges by construction. (So either an abstraction of + 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

Value that can be passed to merge_distinct_bits as the starting value. This value must be neutral wrt. merging of values.

val anisotropic_cast : size:Integer.t -> t -> t

Optionnally change the representation of the given value, under the assumption that it fits in size bits. Returning the value argument is alwas correct.