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.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
.
val unknown :
?attrs:LibraryDesc.attr list ->
(LibraryDesc.special, LibraryDesc.special) args_desc ->
LibraryDesc.t
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.
val r : LibraryDesc.Access.t
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 : LibraryDesc.Access.t
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 : LibraryDesc.Access.t
Shallow AccessKind.t.Write
access.
val w_deep : LibraryDesc.Access.t
Deep AccessKind.t.Write
access. Rarely needed.
val f : LibraryDesc.Access.t
Shallow AccessKind.t.Free
access.
val f_deep : LibraryDesc.Access.t
Deep AccessKind.t.Free
access. Rarely needed.
val s : LibraryDesc.Access.t
Shallow AccessKind.t.Spawn
access.
val s_deep : LibraryDesc.Access.t
Deep AccessKind.t.Spawn
access. Rarely needed.