package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
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, '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 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.