package goblint

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 = {
  1. overflow : bool;
  2. 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 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

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"

OCaml

Innovation. Community. Security.