ApronDomain (goblint.Goblint

module M = Messages

Resources for working with Apron:

OCaml API docs: https://antoinemine.github.io/Apron/doc/api/ocaml/index.html
C API docs (better function descriptions): https://antoinemine.github.io/Apron/doc/api/c/index.html
CEA 2007 slides (overview, mathematical descriptions): https://antoinemine.github.io/Apron/doc/papers/expose_CEA_2007.pdf
C API docs PDF (alternative mathematical descriptions): https://antoinemine.github.io/Apron/doc/api/c/apron.pdf
heterogeneous environments: https://link.springer.com/chapter/10.1007%2F978-3-030-17184-1_26 (Section 4.1)

val widening_thresholds_apron : Apron.Scalar.t array ResettableLazy.t

val reset_lazy : unit -> unit

module V = RelationDomain.V

module type Manager = sig ... end

module OctagonManager : sig ... end

Manager for the Oct domain, i.e. an octagon domain. For Documentation for the domain see: https://antoinemine.github.io/Apron/doc/api/ocaml/Oct.html

module PolyhedraManager : sig ... end

Manager for the Polka domain, i.e. a polyhedra domain. For Documentation for the domain see: https://antoinemine.github.io/Apron/doc/api/ocaml/Polka.html

module AffEqManager : sig ... end

Another manager for the Polka domain but specifically for affine equalities. For Documentation for the domain see: https://antoinemine.github.io/Apron/doc/api/ocaml/Polka.html

module IntervalManager : sig ... end

Manager for the Box domain, i.e. an interval domain. For Documentation for the domain see: https://antoinemine.github.io/Apron/doc/api/ocaml/Box.html

val manager : (module Manager) lazy_t

val get_manager : unit -> (module Manager)

module A = GobApron.Abstract1

module Bounds (Man : Manager) : sig ... end

module type AOpsPure = sig ... end

Pure environment and transfer functions.

module type AOpsImperative = sig ... end

Imperative in-place environment and transfer functions.

module type AOpsImperativeCopy = sig ... end

module AOpsPureOfImperative
  (AOpsImperative : AOpsImperativeCopy) : 
  AOpsPure with type t = AOpsImperative.t

Default implementations of pure functions from copy and imperative functions.

module type AOpsExtra = sig ... end

Extra functions that don't have the pure-imperative correspondence.

module type AOps = sig ... end

module AOps0 (Tracked : RelationDomain.Tracked) (Man : Manager) : sig ... end

Convenience operations on A.

module AOps (Tracked : RelationDomain.Tracked) (Man : Manager) : sig ... end

module type SPrintable = sig ... end

module DBase (Man : Manager) : SPrintable with type t = Man.mt A.t

module type SLattice = sig ... end

module DWithOps
  (Man : Manager)
  (D : SLattice with type t = Man.mt A.t) : 
  sig ... end

module DHetero (Man : Manager) : SLattice with type t = Man.mt A.t

With heterogeneous environments.

module type S2 = sig ... end

module D (Man : Manager) : sig ... end

module OctagonD : sig ... end

module type S3 = sig ... end

module D2 (Man : Manager) : S2 with module Man = Man

module BoxProd0 (D : S3) : sig ... end

Lift D to a non-reduced product with box. Both are updated in parallel, but D answers to queries. Box domain is used to filter out non-relational invariants for output.

module BoxProd (D : S3) : RelationDomain.RD