package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 and TrivialWithLength based on the value of exp.partition-arrays.