ArrayDomain (goblint.ArrayDomain)

module VDQ = ValueDomainQueries

type domain =

| TrivialDomain
| PartitionedDomain
| UnrolledDomain

val get_domain : 
  varAttr:GoblintCil.Cil.attributes ->
  typAttr:GoblintCil.Cil.attributes ->
  domain

gets the underlying domain: chosen by the attributes in AttributeConfiguredArrayDomain

val can_recover_from_top : domain -> bool

Some domains such as Trivial cannot recover from their value ever being top. ValueDomain handles intialization differently for these

module type S0 = sig ... end

module type S = sig ... end

Abstract domains representing arrays.

module type Str = sig ... end

Abstract domains representing strings a.k.a. null-terminated char arrays.

module type StrWithDomain = sig ... end

module type LatticeWithInvalidate = sig ... end

module type LatticeWithSmartOps = sig ... end

module type Null = sig ... end

module type LatticeWithNull = sig ... end

module Trivial
  (Val : LatticeWithInvalidate)
  (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 : LatticeWithInvalidate)
  (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.

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

Like partitioned but additionally manages the length of the array.

module NullByte
  (Val : LatticeWithNull)
  (Idx : IntDomain.Z) : 
  Str with type value = Val.t and type idx = Idx.t

This functor creates an array representation by the indexes of all null bytes * the array must and may contain. This is useful to analyze strings, i.e. null- * terminated char arrays, and particularly to determine if operations on strings * could lead to a buffer overflow. Concrete values from Val are not interesting * for this domain. It additionally tracks the array size.

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

Switches between PartitionedWithLength, TrivialWithLength and Unroll based on variable, type, and flag.

module AttributeConfiguredAndNullByteArrayDomain
  (Val : LatticeWithNull)
  (Idx : IntDomain.Z) : 
  StrWithDomain with type value = Val.t and type idx = Idx.t

Like FlagHelperAttributeConfiguredArrayDomain but additionally runs NullByte * in parallel if flag "ana.base.arrays.nullbytes" is set.