package goblint

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

Abstract domains for C arrays.

module VDQ = ValueDomainQueries
type domain =
  1. | TrivialDomain
  2. | PartitionedDomain
  3. | 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.

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.

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.

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

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

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