package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

Dune Dependency

Authors

Maintainers

Sources

goblint-2.0.0.tbz
sha256=2f4f2e25b765452f0e336941f35f6cb396d7c213a2d347abe5d35febc5159b1f
sha512=e96af4cad91f6985c8db93c194925853e96cad0ec1a0d9f4d32bbe16d3e5fa1e305f54be02839f21ba89ad2af0c2d5d7aa819ade221ce097dc4dbd0fcd8c8500

doc/goblint.lib/Goblint_lib/ArrayDomain/index.html

Module Goblint_lib.ArrayDomain

module type S = sig ... end

Abstract domains representing arrays.

module type LatticeWithSmartOps = sig ... end
module Trivial (Val : Lattice.S) (Idx : Lattice.S) : S with type value = Val.t and type idx = Idx.t

This functor creates a trivial single cell representation of an array. The * indexing type is taken as a parameter to satisfy the type system, it is not * used in the implementation.

module TrivialWithLength (Val : Lattice.S) (Idx : IntDomain.Z) : S with type value = Val.t and type idx = Idx.t

This functor creates a trivial single cell representation of an array. The * indexing type is also used to manage the length.

module Partitioned (Val : LatticeWithSmartOps) (Idx : IntDomain.Z) : S with type value = Val.t and type idx = Idx.t

This functor creates an array representation that allows for partitioned arrays * Such an array can be partitioned according to an expression in which case it * uses three values from Val to represent the elements of the array to the left, * at, and to the right of the expression. The Idx domain is required only so to * have a signature that allows for choosing an array representation at runtime.

Like partitioned but additionally manages the length of the array.

Switches between PartitionedWithLength, TrivialWithLength and Unroll based on the value of ana.base.arrays.domain.

OCaml

Innovation. Community. Security.