Module Frama_c_kernel.Int_interval

Integer intervals with congruence. An interval defined by min, max, rem, modu represents all integers between the bounds min and max and congruent to rem modulo modu. A value of None for min (resp. max) represents -infinity (resp. +infinity). modu is > 0, and 0 <= rem < modu.

include Datatype.S_with_collections
include Datatype.S
include Datatype.S_no_copy
include Datatype.Ty
type t
module Set : Datatype.Set with type elt = t
module Map : Datatype.Map with type key = t
module Hashtbl : Datatype.Hashtbl with type key = t
include Eva_lattice_type.Full_AI_Lattice_with_cardinality with type t := t and type widen_hint = Integer.t * Datatype.Integer.Set.t
include Eva_lattice_type.AI_Lattice_with_cardinal_one with type t := t with type widen_hint = Integer.t * Datatype.Integer.Set.t
include Eva_lattice_type.Join_Semi_Lattice with type t := t

datatype of element of the lattice

include Datatype.S with type t := t
include Datatype.S_no_copy with type t := t
include Datatype.Ty with type t := 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?

include Eva_lattice_type.With_Top with type t := t
val top : t

largest element

include Eva_lattice_type.With_Widening with type t := t with type widen_hint = Integer.t * Datatype.Integer.Set.t
type widen_hint = Integer.t * Datatype.Integer.Set.t

hints for the widening

val widen : widen_hint -> t -> t -> t

widen h t1 t2 is an over-approximation of join t1 t2. Assumes is_included t1 t2

include Eva_lattice_type.With_Cardinal_One with type t := t
val cardinal_zero_or_one : t -> bool
include Eva_lattice_type.With_Narrow with type t := t
val narrow : t -> t -> t Lattice_bounds.or_bottom

over-approximation of intersection

include Eva_lattice_type.With_Under_Approximation with type t := t

under-approximation of union

val meet : t -> t -> t Lattice_bounds.or_bottom

under-approximation of intersection

include Eva_lattice_type.With_Intersects with type t := t
val intersects : t -> t -> bool

intersects t1 t2 returns true iff the intersection of t1 and t2 is non-empty.

include Eva_lattice_type.With_Diff with type t := t
val diff : t -> t -> t Lattice_bounds.or_bottom

diff t1 t2 is an over-approximation of t1-t2. t2 must be an under-approximation or exact.

include Eva_lattice_type.With_Diff_One with type t := t
val diff_if_one : t -> t -> t Lattice_bounds.or_bottom

diff_if_one t1 t2 is an over-approximation of t1-t2.

  • returns

    t1 if t2 is not a singleton.

include Eva_lattice_type.With_Enumeration with type t := t
val fold_enum : (t -> 'a -> 'a) -> t -> 'a -> 'a

Fold on the elements of the value one by one if possible. Raises Abstract_interp.Not_less_than when there is an infinite number of elements to enumerate.

val cardinal_less_than : t -> int -> int

Raises Abstract_interp.Not_less_than whenever the cardinal of the given lattice is strictly higher than the given integer.

val check : min:Integer.t option -> max:Integer.t option -> rem:Integer.t -> modu:Integer.t -> unit

Checks that the interval defined by min, max, rem, modu is well formed.

val make : min:Integer.t option -> max:Integer.t option -> rem:Integer.t -> modu:Integer.t -> t

Makes the interval of all integers between min and max and congruent to rem modulo modu. Fails if these conditions does not hold:

  • min ≤ max
  • 0 ≤ rem < modu
  • min ≅ rem modu ∧ max ≅ rem modu
val inject_range : Integer.t option -> Integer.t option -> t

Makes the interval of all integers between min and max.

val min_and_max : t -> Integer.t option * Integer.t option

Returns the bounds of the given interval. None means infinity.

val min_max_rem_modu : t -> Integer.t option * Integer.t option * Integer.t * Integer.t

Returns the bounds and the modulo of the given interval.

val mem : Integer.t -> t -> bool

mem i t returns true iff the integer i is in the interval t.

val cardinal : t -> Integer.t option

Returns the number of integers represented by the given interval. Returns None if the interval represents an infinite number of integers.

val complement_under : min:Integer.t -> max:Integer.t -> t -> t Lattice_bounds.or_bottom

Returns an under-approximation of the integers between min and max that are *not* represented by the given interval.

Interval semantics.

See Int_val for more details.

val add_singleton_int : Integer.t -> t -> t
val add : t -> t -> t
val add_under : t -> t -> t Lattice_bounds.or_bottom
val neg : t -> t
val abs : t -> t
val scale : Integer.t -> t -> t
val scale_div : pos:bool -> Integer.t -> t -> t
val scale_div_under : pos:bool -> Integer.t -> t -> t Lattice_bounds.or_bottom
val scale_rem : pos:bool -> Integer.t -> t -> t
val mul : t -> t -> t
val div : t -> t -> t Lattice_bounds.or_bottom
val c_rem : t -> t -> t Lattice_bounds.or_bottom
val cast : size:Integer.t -> signed:bool -> t -> t

Misc.

val subdivide : t -> t * t
val reduce_sign : t -> bool -> t Lattice_bounds.or_bottom
val reduce_bit : int -> t -> bool -> t Lattice_bounds.or_bottom
val fold_int : ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
val to_seq : ?increasing:bool -> t -> Integer.t Seq.t