Module `Goblint_lib.LibraryDesc`

Library function descriptor (specification).

module Cil = GoblintCil

Pointer argument access specification.

module Access : sig ... end

Pointer argument access specification.

type math =

| Nan of CilType.Fkind.t * Basetype.CilExp.t
| Inf of CilType.Fkind.t
| Isfinite of Basetype.CilExp.t
| Isinf of Basetype.CilExp.t
| Isnan of Basetype.CilExp.t
| Isnormal of Basetype.CilExp.t
| Signbit of Basetype.CilExp.t
| Isgreater of Basetype.CilExp.t * Basetype.CilExp.t
| Isgreaterequal of Basetype.CilExp.t * Basetype.CilExp.t
| Isless of Basetype.CilExp.t * Basetype.CilExp.t
| Islessequal of Basetype.CilExp.t * Basetype.CilExp.t
| Islessgreater of Basetype.CilExp.t * Basetype.CilExp.t
| Isunordered of Basetype.CilExp.t * Basetype.CilExp.t
| Ceil of CilType.Fkind.t * Basetype.CilExp.t
| Floor of CilType.Fkind.t * Basetype.CilExp.t
| Fabs of CilType.Fkind.t * Basetype.CilExp.t
| Fmax of CilType.Fkind.t * Basetype.CilExp.t * Basetype.CilExp.t
| Fmin of CilType.Fkind.t * Basetype.CilExp.t * Basetype.CilExp.t
| Acos of CilType.Fkind.t * Basetype.CilExp.t
| Asin of CilType.Fkind.t * Basetype.CilExp.t
| Atan of CilType.Fkind.t * Basetype.CilExp.t
| Atan2 of CilType.Fkind.t * Basetype.CilExp.t * Basetype.CilExp.t
| Cos of CilType.Fkind.t * Basetype.CilExp.t
| Sin of CilType.Fkind.t * Basetype.CilExp.t
| Tan of CilType.Fkind.t * Basetype.CilExp.t

val equal_math : math -> math -> Ppx_deriving_runtime.bool

val compare_math : math -> math -> Ppx_deriving_runtime.int

val hash_math : math -> int

type special =

| Malloc of Cil.Cil.exp
| Calloc of {
1. count : Cil.Cil.exp;
2. size : Cil.Cil.exp;
}
| Realloc of {
1. ptr : Cil.Cil.exp;
2. size : Cil.Cil.exp;
}
| Free of Cil.Cil.exp
| Assert of {
1. exp : Cil.Cil.exp;
2. check : bool;
3. refine : bool;
}
| Lock of {
1. lock : Cil.Cil.exp;
2. try_ : bool;
3. write : bool;
4. return_on_success : bool;
}
| Unlock of Cil.Cil.exp
| ThreadCreate of {
1. thread : Cil.Cil.exp;
2. start_routine : Cil.Cil.exp;
3. arg : Cil.Cil.exp;
}
| ThreadJoin of {
1. thread : Cil.Cil.exp;
2. ret_var : Cil.Cil.exp;
}
| ThreadExit of {
1. ret_val : Cil.Cil.exp;
}
| Signal of Cil.Cil.exp
| Broadcast of Cil.Cil.exp
| MutexAttrSetType of {
1. attr : Cil.Cil.exp;
2. typ : Cil.Cil.exp;
}
| MutexInit of {
1. mutex : Cil.Cil.exp;
2. attr : Cil.Cil.exp;
}
| Wait of {
1. cond : Cil.Cil.exp;
2. mutex : Cil.Cil.exp;
}
| TimedWait of {
1. cond : Cil.Cil.exp;
2. mutex : Cil.Cil.exp;
3. abstime : Cil.Cil.exp;
  (*
  Unused
  *)
}
| Math of {
1. fun_args : math;
}
| Memset of {
1. dest : Cil.Cil.exp;
2. ch : Cil.Cil.exp;
3. count : Cil.Cil.exp;
}
| Bzero of {
1. dest : Cil.Cil.exp;
2. count : Cil.Cil.exp;
}
| Memcpy of {
1. dest : Cil.Cil.exp;
2. src : Cil.Cil.exp;
}
| Strcpy of {
1. dest : Cil.Cil.exp;
2. src : Cil.Cil.exp;
3. n : Cil.Cil.exp option;
}
| Strcat of {
1. dest : Cil.Cil.exp;
2. src : Cil.Cil.exp;
3. n : Cil.Cil.exp option;
}
| Strlen of Cil.Cil.exp
| Strstr of {
1. haystack : Cil.Cil.exp;
2. needle : Cil.Cil.exp;
}
| Strcmp of {
1. s1 : Cil.Cil.exp;
2. s2 : Cil.Cil.exp;
3. n : Cil.Cil.exp option;
}
| Abort
| Identity of Cil.Cil.exp
(*
Identity function. Some compiler optimization annotation functions map to this.
*)
| Setjmp of {
1. env : Cil.Cil.exp;
}
| Longjmp of {
1. env : Cil.Cil.exp;
2. value : Cil.Cil.exp;
}
| Rand
| 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.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.Cil.exp list ->
    [< `Calloc of Cil.Cil.exp * Cil.Cil.exp
    | `Lock of bool * bool * bool
    | `Malloc of Cil.Cil.exp
    | `Realloc of Cil.Cil.exp * Cil.Cil.exp
    | `ThreadCreate of Cil.Cil.exp * Cil.Cil.exp * Cil.Cil.exp
    | `ThreadJoin of Cil.Cil.exp * Cil.Cil.exp
    | `Unknown of 'a
    | `Unlock ]) ->
  Cil.Cil.exp list ->
  special

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

module MathPrintable : sig ... end

module MathLifted : sig ... end

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`