package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

Dune Dependency

Authors

Maintainers

Sources

goblint-2.0.1.tbz
sha256=dba2b664c7c125687e708e871d83fbfb6ba6d9ee98d235b4850d9a238caa84de
sha512=529987cde39691ad9e955000a3603e89c1c8cf14ed5e8b4cd3a7fc26e47d016aff571b472e2329725133c46f8d0cb45a05b88994eeffaa221a4d31b4c543adcd

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.