Module `IntDomain`

Abstract domains for C integers.

val should_wrap : GoblintCil.Cil.ikind -> bool

val should_ignore_overflow : GoblintCil.Cil.ikind -> bool

val reset_lazy : unit -> unit

type overflow_info = {

overflow : bool;
underflow : bool;

}

module type Arith = sig ... end

module type ArithIkind = sig ... end

module type B = sig ... end

The signature of integral value domains. They need to support all integer * operations that are allowed in C

module type IkindUnawareS = sig ... end

Interface of IntDomain implementations that do not take ikinds for arithmetic operations yet. TODO: Should be ported to S in the future.

module type S = sig ... end

Interface of IntDomain implementations taking an ikind for arithmetic operations

module type SOverflow = sig ... end

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

module type Y = sig ... end

The signature of integral value domains keeping track of ikind information

module type Z = Y with type int_t = Z.t

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

module type Ikind = sig ... end

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 IntervalSetFunctor
  (Ints_t : IntOps.IntOps) : 
  SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) list

module Interval32 : Y with type int_t = IntOps.Int64Ops.t

module Interval : 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.

module Reverse
  (Base : IkindUnawareS) : 
  IkindUnawareS with type t = Base.t and type int_t = Base.int_t

Reverses bot, top, leq, join, meet

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

Boolean domains

module type BooleansNames = sig ... end

Parameter signature for the MakeBooleans functor.

module MakeBooleans (Names : BooleansNames) : IkindUnawareS with type t = bool

Creates an abstract domain for integers represented by boolean values.

module Booleans : IkindUnawareS with type t = bool

Boolean abstract domain, where true is output "True" and false is output * "False"

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/goblint_cdomain_value/IntDomain/index.html

Module `IntDomain`

package goblint

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/goblint_cdomain_value/IntDomain/index.html

Module IntDomain

dune-project
Dependency

Module `IntDomain`