Module `Goblint_lib.LibraryDesc`

module Cil = GoblintCil

Library function descriptor (specification).

module Access : sig ... end

Pointer argument access specification.

type math =

| Nan of Cil.fkind * Cil.exp
| Inf of Cil.fkind
| Isfinite of Cil.exp
| Isinf of Cil.exp
| Isnan of Cil.exp
| Isnormal of Cil.exp
| Signbit of Cil.exp
| Isgreater of Cil.exp * Cil.exp
| Isgreaterequal of Cil.exp * Cil.exp
| Isless of Cil.exp * Cil.exp
| Islessequal of Cil.exp * Cil.exp
| Islessgreater of Cil.exp * Cil.exp
| Isunordered of Cil.exp * Cil.exp
| Ceil of Cil.fkind * Cil.exp
| Floor of Cil.fkind * Cil.exp
| Fabs of Cil.fkind * Cil.exp
| Fmax of Cil.fkind * Cil.exp * Cil.exp
| Fmin of Cil.fkind * Cil.exp * Cil.exp
| Acos of Cil.fkind * Cil.exp
| Asin of Cil.fkind * Cil.exp
| Atan of Cil.fkind * Cil.exp
| Atan2 of Cil.fkind * Cil.exp * Cil.exp
| Cos of Cil.fkind * Cil.exp
| Sin of Cil.fkind * Cil.exp
| Tan of Cil.fkind * Cil.exp

type special =

| Malloc of Cil.exp
| Calloc of {
1. count : Cil.exp;
2. size : Cil.exp;
}
| Realloc of {
1. ptr : Cil.exp;
2. size : Cil.exp;
}
| Assert of {
1. exp : Cil.exp;
2. check : bool;
3. refine : bool;
}
| Lock of {
1. lock : Cil.exp;
2. try_ : bool;
3. write : bool;
4. return_on_success : bool;
}
| Unlock of Cil.exp
| ThreadCreate of {
1. thread : Cil.exp;
2. start_routine : Cil.exp;
3. arg : Cil.exp;
}
| ThreadJoin of {
1. thread : Cil.exp;
2. ret_var : Cil.exp;
}
| ThreadExit of {
1. ret_val : Cil.exp;
}
| Signal of Cil.exp
| Broadcast of Cil.exp
| Wait of {
1. cond : Cil.exp;
2. mutex : Cil.exp;
}
| TimedWait of {
1. cond : Cil.exp;
2. mutex : Cil.exp;
3. abstime : Cil.exp;
  (*
  Unused
  *)
}
| Math of {
1. fun_args : math;
}
| Memset of {
1. dest : Cil.exp;
2. ch : Cil.exp;
3. count : Cil.exp;
}
| Bzero of {
1. dest : Cil.exp;
2. count : Cil.exp;
}
| Memcpy of {
1. dest : Cil.exp;
2. src : Cil.exp;
}
| Strcpy of {
1. dest : Cil.exp;
2. src : Cil.exp;
}
| Abort
| Identity of Cil.exp
(*
Identity function. Some compiler optimization annotation functions map to this.
*)
| Unknown
(*
Anything not belonging to other types.
*)

Type of special function, or Unknown.

module Accesses : sig ... end

Pointer arguments access specification.

type attr =

| ThreadUnsafe
(*
Function is not thread-safe to call, e.g. due to its own internal (global) state.
- see https://man7.org/linux/man-pages/man7/pthreads.7.html
  for list of thread-unsafe functions under POSIX.
- see https://github.com/goblint/analyzer/issues/723
  for Goblint issue about the (future) use of this attribute.
*)
| InvalidateGlobals
(*
Function invalidates all globals when called.
*)

Function attribute.

type t = {

special : Cil.exp list -> special;
(*
Conversion to special using arguments.
*)
accs : Accesses.t;
(*
Pointer arguments access specification.
*)
attrs : attr list;
(*
Attributes of function.
*)

}

Library function descriptor.

val special_of_old : 
  (Cil.exp list ->
    [< `Calloc of Cil.exp * Cil.exp
    | `Lock of bool * bool * bool
    | `Malloc of Cil.exp
    | `Realloc of Cil.exp * Cil.exp
    | `ThreadCreate of Cil.exp * Cil.exp * Cil.exp
    | `ThreadJoin of Cil.exp * Cil.exp
    | `Unknown of 'a
    | `Unlock ]) ->
  Cil.exp list ->
  special

val of_old : 
  ?attrs:attr list ->
  Accesses.old ->
  (Cil.exp list ->
    [< `Calloc of Cil.exp * Cil.exp
    | `Lock of bool * bool * bool
    | `Malloc of Cil.exp
    | `Realloc of Cil.exp * Cil.exp
    | `ThreadCreate of Cil.exp * Cil.exp * Cil.exp
    | `ThreadJoin of Cil.exp * Cil.exp
    | `Unknown of 'a
    | `Unlock ]) ->
  t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/LibraryDesc/index.html

Module `Goblint_lib.LibraryDesc`

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/LibraryDesc/index.html

Module Goblint_lib.LibraryDesc

Module `Goblint_lib.LibraryDesc`