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.0.0.tbz
sha256=2f4f2e25b765452f0e336941f35f6cb396d7c213a2d347abe5d35febc5159b1f
sha512=e96af4cad91f6985c8db93c194925853e96cad0ec1a0d9f4d32bbe16d3e5fa1e305f54be02839f21ba89ad2af0c2d5d7aa819ade221ce097dc4dbd0fcd8c8500

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

Module Goblint_lib.LibraryDsl

See LibraryFunctions implementation for example usage.

Library function descriptor DSL.

Type parameters in this module can be ignored for usage. They are inferred automatically and used to ensure type-safety.

type ('k, 'l, 'r) arg_desc

Argument descriptor.

type ('k, 'r) args_desc =
  1. | [] : ('r, 'r) args_desc
    (*

    End of arguments. No more arguments may occur.

    *)
  2. | VarArgs : (_, 'l, 'r) arg_desc -> ('l, 'r) args_desc
    (*

    Variadic arguments, all with the same argument descriptor. Any number of arguments (including 0) may occur.

    *)
  3. | :: : ('k, _, 'm) arg_desc * ('m, 'r) args_desc -> ('k, 'r) args_desc
    (*

    Cons one argument descriptor. Argument must occur.

    *)

Arguments descriptor. Overrides standard list syntax.

val special : ?attrs:LibraryDesc.attr list -> ('k, LibraryDesc.special) args_desc -> 'k -> LibraryDesc.t

Create library function descriptor from arguments descriptor and continuation function, which takes as many arguments as are captured using __ and returns the corresponding LibraryDesc.special.

Create unknown library function descriptor from arguments descriptor, which must drop all arguments.

val __ : string -> LibraryDesc.Access.t list -> (GoblintCil.Cil.exp -> 'r, GoblintCil.Cil.exp list -> 'r, 'r) arg_desc

Argument descriptor, which captures the named argument with accesses for continuation function of special.

val __' : LibraryDesc.Access.t list -> (GoblintCil.Cil.exp -> 'r, GoblintCil.Cil.exp list -> 'r, 'r) arg_desc

Argument descriptor, which captures an unnamed argument with accesses for continuation function of special.

val drop : string -> LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_desc

Argument descriptor, which drops (does not capture) the named argument with accesses.

val drop' : LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_desc

Argument descriptor, which drops (does not capture) an unnamed argument with accesses.

Shallow AccessKind.t.Read access. All immediate arguments of function calls are always read, this specifies the reading of pointed-to values.

Deep AccessKind.t.Read access. All immediate arguments of function calls are always read, this specifies the reading of pointed-to values. Rarely needed.

Shallow AccessKind.t.Write access.

Deep AccessKind.t.Write access. Rarely needed.

Shallow AccessKind.t.Free access.

Deep AccessKind.t.Free access. Rarely needed.

Shallow AccessKind.t.Spawn access.

Deep AccessKind.t.Spawn access. Rarely needed.