package goblint

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

Module LibraryDslSource

Library function descriptor DSL.

See LibraryFunctions implementation for example usage.

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

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

Argument descriptor.

Sourcetype ('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.

Sourceval 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 library function descriptor from arguments descriptor, which must drop all arguments, and continuation function, which takes as an unit argument and returns the corresponding LibraryDesc.special. Unlike special, this allows the LibraryDesc.special of an argumentless function to depend on options, such that they aren't evaluated at initialization time in LibraryFunctions.

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

Sourcetype access

Argument access descriptor.

Sourceval __ : string -> access 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.

Sourceval __' : access 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.

Sourceval drop : string -> access list -> ('r, 'r, 'r) arg_desc

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

Sourceval drop' : access list -> ('r, 'r, 'r) arg_desc

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

Sourceval r : access

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

Sourceval r_deep : access

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

Sourceval w : access

Shallow AccessKind.t.Write access.

Sourceval w_deep : access

Deep AccessKind.t.Write access. Rarely needed.

Sourceval f : access

Shallow AccessKind.t.Free access.

Sourceval f_deep : access

Deep AccessKind.t.Free access. Rarely needed.

Sourceval s : access

Shallow AccessKind.t.Spawn access.

Sourceval s_deep : access

Deep AccessKind.t.Spawn access. Rarely needed.

Sourceval c : access

Shallow AccessKind.t.Spawn access, substituting function pointer calls for now (TODO).

Sourceval c_deep : access

Deep AccessKind.t.Spawn access, substituting deep function pointer calls for now (TODO)

Sourceval if_ : (unit -> bool) -> access -> access

Conditional access, e.g. on an option.

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