package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=452d8491527aea21f2cbb11defcc14ba0daf9fdb6bdb9fc0af73e56eac57b916
sha512=1993cd45c4c7fe124ca6e157f07d17ec50fab5611b270a434ed1b7fb2910aa85a8e6eaaa77dad770430710aafb2f6d676c774dd33942d921f23e2f9854486551
doc/goblint.library/LibraryDsl/index.html
Module LibraryDsl
Source
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.
Argument descriptor.
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 special' :
?attrs:LibraryDesc.attr list ->
(LibraryDesc.special, LibraryDesc.special) args_desc ->
(unit -> LibraryDesc.special) ->
LibraryDesc.t
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
.
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.
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
.
Argument descriptor, which drops (does not capture) the named argument with accesses.
Argument descriptor, which drops (does not capture) an unnamed argument with accesses.
Shallow AccessKind.t.Read
access. All immediate arguments of function calls are always read, this specifies the reading of pointed-to values.
Deep AccessKind.t.Read
access. All immediate arguments of function calls are always read, this specifies the reading of pointed-to values. Rarely needed.
Shallow AccessKind.t.Write
access.
Deep AccessKind.t.Write
access. Rarely needed.
Shallow AccessKind.t.Free
access.
Deep AccessKind.t.Free
access. Rarely needed.
Shallow AccessKind.t.Spawn
access.
Deep AccessKind.t.Spawn
access. Rarely needed.
Shallow AccessKind.t.Spawn
access, substituting function pointer calls for now (TODO).
Deep AccessKind.t.Spawn
access, substituting deep function pointer calls for now (TODO)