package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=bfc412ec2e447eaef6f4f83892e3511ebf305593cb00561c1406be3ae8bf48e9
sha512=5f2a162e5f36bffafc9836b0d18b5b2808cecfa6bf68f83bb7d1e8b9947ac74cf07776eb09274b4b29d55c897a45a10768f0d9ed25810cf6ba2409c525e4cd4d
doc/goblint.lib/Goblint_lib/LibraryDsl/index.html
Module Goblint_lib.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, 'r) args_desc = | [] : ('r, 'r) args_desc(*End of arguments. No more arguments may occur.
*)| 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.
*)| :: : ('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.tCreate library function descriptor from arguments descriptor and continuation function, which takes as many arguments as are captured using __ and returns the corresponding LibraryDesc.special.
val special' :
?attrs:LibraryDesc.attr list ->
(LibraryDesc.special, LibraryDesc.special) args_desc ->
(unit -> LibraryDesc.special) ->
LibraryDesc.tCreate 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.
val unknown :
?attrs:LibraryDesc.attr list ->
(LibraryDesc.special, LibraryDesc.special) args_desc ->
LibraryDesc.tCreate 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_descArgument 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_descArgument descriptor, which captures an unnamed argument with accesses for continuation function of special.
val drop : string -> LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_descArgument descriptor, which drops (does not capture) the named argument with accesses.
val drop' : LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_descArgument descriptor, which drops (does not capture) an unnamed argument with accesses.
val r : LibraryDesc.Access.tShallow AccessKind.t.Read access. All immediate arguments of function calls are always read, this specifies the reading of pointed-to values.
val r_deep : LibraryDesc.Access.tDeep 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 : LibraryDesc.Access.tShallow AccessKind.t.Write access.
val w_deep : LibraryDesc.Access.tDeep AccessKind.t.Write access. Rarely needed.
val f : LibraryDesc.Access.tShallow AccessKind.t.Free access.
val f_deep : LibraryDesc.Access.tDeep AccessKind.t.Free access. Rarely needed.
val s : LibraryDesc.Access.tShallow AccessKind.t.Spawn access.
val s_deep : LibraryDesc.Access.tDeep AccessKind.t.Spawn access. Rarely needed.