package goblint

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

Abstract domains representing sets.

module GU = Goblintutil
exception Unsupported of string
val unsupported : string -> 'a
module type S = sig ... end

A set domain must support all the standard library set operations. They have been copied instead of included since our empty has a different signature.

module Blank : sig ... end

A functor for creating a simple set domain, there is no top element, and * calling top () will raise an exception

module Make (Base : Printable.S) : S with type elt = Base.t and type t = BatSet.Make(Base).t

A functor for creating a simple set domain, there is no top element, and * calling top () will raise an exception

A functor for creating a path sensitive set domain, that joins the base * analysis whenever the user elements coincide. Just as above there is no top * element, and calling top () will raise an exception

module Sensitive (Base : Lattice.S) (User : Printable.S) : sig ... end
module type ToppedSetNames = sig ... end

Auxiliary signature for naming the top element

module LiftTop (S : S) (N : ToppedSetNames) : S with type elt = S.elt and type t = [ `Top | `Lifted of S.t ]
module ToppedSet (Base : Printable.S) (N : ToppedSetNames) : S with type elt = Base.t and type t = [ `Top | `Lifted of Make(Base).t ]

Functor for creating artificially topped set domains.

module HeadlessSet (Base : Printable.S) : sig ... end
module Reverse (Base : S) : sig ... end

Reverses lattice order of a set domain while keeping the set operations same.

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