package goblint

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

Abstract Domains for integers. These are domains that support the C * operations on integer values.

val should_wrap : GoblintCil.Cil.ikind -> bool
val should_ignore_overflow : GoblintCil.Cil.ikind -> bool
val reset_lazy : unit -> unit
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 OldDomainFacade (Old : IkindUnawareS with type int_t = int64) : S with type int_t = IntOps.BigIntOps.t and type t = Old.t

Facade for IntDomain implementations that do not implement the interface where arithmetic functions take an ikind parameter.

module type Y = sig ... end

The signature of integral value domains keeping track of ikind information

module type Z = Y with type int_t = IntOps.BigIntOps.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 : (GoblintCil.Cilint.cilint * 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 FlattenedBI : IkindUnawareS with type t = [ `Top | `Lifted of IntOps.BigIntOps.t | `Bot ] and type int_t = IntOps.BigIntOps.t

This is the typical flattened integer domain used in Kildall's constant * propagation, using Big_int instead of int64.

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) : S with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option
module Interval32 : Y with type int_t = IntOps.Int64Ops.t
module BigInt : sig ... end
module Interval : S with type int_t = IntOps.BigIntOps.t
module Congruence : S with type int_t = IntOps.BigIntOps.t
module DefExc : S with type int_t = IntOps.BigIntOps.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 = IntOps.BigIntOps.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"