package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=dba2b664c7c125687e708e871d83fbfb6ba6d9ee98d235b4850d9a238caa84de
sha512=529987cde39691ad9e955000a3603e89c1c8cf14ed5e8b4cd3a7fc26e47d016aff571b472e2329725133c46f8d0cb45a05b88994eeffaa221a4d31b4c543adcd
doc/goblint.lib/Goblint_lib/IntDomain/index.html
Module Goblint_lib.IntDomain
Abstract Domains for integers. These are domains that support the C * operations on integer values.
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 type Ikind = sig ... end
module PtrDiffIkind : Ikind
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
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.
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
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 join
ing or meet
ing 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"