Module LibraryDsl

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.

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 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.

type access

Argument access descriptor.

val __ : 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.

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

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

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

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

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

val r : access

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

val 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.

val w : access

Shallow AccessKind.t.Write access.

val w_deep : access

Deep AccessKind.t.Write access. Rarely needed.

val f : access

Shallow AccessKind.t.Free access.

val f_deep : access

Deep AccessKind.t.Free access. Rarely needed.

val s : access

Shallow AccessKind.t.Spawn access.

val s_deep : access

Deep AccessKind.t.Spawn access. Rarely needed.

val c : access

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

val c_deep : access

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

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

Conditional access, e.g. on an option.

exception Expected of string