IntDomain (goblint.IntDomain)

val should_wrap : GoblintCil.Cil.ikind -> bool

val should_ignore_overflow : GoblintCil.Cil.ikind -> bool

val reset_lazy : unit -> unit

type nonrec overflow_info = IntDomain_intf.overflow_info = {

overflow : bool;
underflow : bool;

}

module type Arith = IntDomain_intf.Arith

module type ArithIkind = IntDomain_intf.ArithIkind

module type B = IntDomain_intf.B

module type IkindUnawareS = IntDomain_intf.IkindUnawareS

module type S = IntDomain_intf.S

module type S2 = IntDomain_intf.S2

module type SOverflow = IntDomain_intf.SOverflow

module SOverflowUnlifter
  (D : SOverflow) : 
  S2 with type int_t = D.int_t and type t = D.t

module type Y = IntDomain_intf.Y

module type Z = IntDomain_intf.Z

module IntDomLifter (I : S2) : Y with type int_t = I.int_t

module type Ikind = IntDomain_intf.Ikind

module PtrDiffIkind : Ikind

module IntDomWithDefaultIkind
  (I : Y)
  (Ik : Ikind) : 
  Y with type t = I.t and type int_t = I.int_t

module IntDomTuple : sig ... end

val of_const : (Z.t * GoblintCil.Cil.ikind * string option) -> IntDomTuple.t

module Size : sig ... end

module BISet : SetDomain.S with type elt = Z.t

exception ArithmeticOnIntegerBot of string

exception Unknown

An exception that can be raised when the result of a computation is unknown. * This is caught by lifted domains and will be replaced by top.

exception Error

An exception that can be raised when an arithmetic error occurs. This is * caught by lifted domains and the evaluation will then be set to bot, which * signifies an error in computation

exception IncompatibleIKinds of string

module Integers
  (Ints_t : IntOps.IntOps) : 
  IkindUnawareS with type t = Ints_t.t and type int_t = Ints_t.t

Predefined domains

module FlatPureIntegers : 
  IkindUnawareS
    with type t = IntOps.Int64Ops.t
     and type int_t = IntOps.Int64Ops.t

The integers with flattened orderings. Calling top and bot or joining or meeting inequal elements will raise exceptions.

module Flattened : 
  IkindUnawareS
    with type t = [ `Top | `Lifted of IntOps.Int64Ops.t | `Bot ]
     and type int_t = IntOps.Int64Ops.t

This is the typical flattened integer domain used in Kildall's constant * propagation.

module Lifted : 
  IkindUnawareS
    with type t = [ `Top | `Lifted of int64 | `Bot ]
     and type int_t = int64

Artificially bounded integers in their natural ordering.

module IntervalFunctor
  (Ints_t : IntOps.IntOps) : 
  SOverflow
    with type int_t = Ints_t.t
     and type t = (Ints_t.t * Ints_t.t) option

module BitfieldFunctor
  (Ints_t : IntOps.IntOps) : 
  SOverflow with type int_t = Ints_t.t and type t = Ints_t.t * Ints_t.t

module IntervalSetFunctor
  (Ints_t : IntOps.IntOps) : 
  SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) list

module Interval : SOverflow with type int_t = Z.t

module Bitfield : SOverflow with type int_t = Z.t

module IntervalSet : SOverflow with type int_t = Z.t

module Congruence : S with type int_t = Z.t

module DefExc : S with type int_t = Z.t

The DefExc domain. The Flattened integer domain is topped by exclusion sets. * Good for analysing branches.

Domain constructors

module Flat
  (Base : IkindUnawareS) : 
  IkindUnawareS
    with type t = [ `Bot | `Lifted of Base.t | `Top ]
     and type int_t = Base.int_t

Creates a flat value domain, where all ordering is lost. Arithmetic * operations are lifted such that only lifted values can be evaluated * otherwise the top/bot is simply propagated with bot taking precedence over * top.

module Lift
  (Base : IkindUnawareS) : 
  IkindUnawareS
    with type t = [ `Bot | `Lifted of Base.t | `Top ]
     and type int_t = Base.int_t

Just like Value.Flat except the order is preserved.

Interval domain with int64-s --- use with caution!

module Enums : S with type int_t = Z.t

Inclusive and exclusive intervals. Warning: NOT A LATTICE