package goblint

  1. Overview
  2. Docs
package goblint
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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct