package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install 

dune-project
 Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (9)

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. R
    Ralf Vogler
  6. K
    Kalmer Apinis
  7. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>

Sources

goblint-2.3.0.tbz
sha256=b729c94adb383a39aea32eb005c988dfd44b92af22ee6a4eedf4239542ac6c26
sha512=643b98770e5fe5644324c95c9ae3a9f698f25c8b11b298f0751d524e0b20af368b2a465fc8200b75a73d48fc9a053fd90f5e8920d4db070927f93188bb8687e0

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

Module Goblint_lib.Offset

Domains for variable offsets, i.e. array indices and struct fields.

type nonrec 'i t = [
  1. | `NoOffset
    (*

    No offset. Marks the end of offset list.

    *)
  2. | `Field of CilType.Fieldinfo.t * 'i Goblint_lib__.Offset_intf.t
    (*

    Offset starting with a struct field.

    *)
  3. | `Index of 'i * 'i Goblint_lib__.Offset_intf.t
    (*

    Offset starting with an array index.

    *)
]

List of nested offsets.

  • parameter 'i

    Type of indices.

val equal : ('i -> 'i -> Ppx_deriving_runtime.bool) -> 'i t -> 'i t -> Ppx_deriving_runtime.bool
val compare : ('i -> 'i -> Ppx_deriving_runtime.int) -> 'i t -> 'i t -> Ppx_deriving_runtime.int
val hash : ('i -> int) -> 'i t -> int
module Index : sig ... end

Domains for offset indices.

exception Type_of_error of GoblintCil.typ * string

Printable.type_of could not follow offset completely.

module type Printable = sig ... end
module type Lattice = sig ... end

Make Printable offset from printable indices.

module MakeLattice (Idx : Index.Lattice) : Lattice with type idx = Idx.t

Make offset Lattice from lattice indices.

module Unit : sig ... end

Offset with Index.Unit indices.

module Exp : sig ... end

Offset with Index.Exp indices.