package goblint

You can search for identifiers within the package.

in-package search v0.2.0

package goblint

Legend:
Library
Module
Module type
Parameter
Class
Class type

Library function descriptor (specification).

module Cil = GoblintCil

Pointer argument access specification.

module Access : sig ... end

Pointer argument access specification.

type math =

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 =

| Alloca of Cil.Cil.exp
| 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;
4. multiple : bool;
}
| ThreadJoin of {
1. thread : Cil.Cil.exp;
2. ret_var : Cil.Cil.exp;
}
| ThreadExit of {
1. ret_val : Cil.Cil.exp;
}
| Globalize of 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;
}
| SemInit of {
1. sem : Cil.Cil.exp;
2. pshared : Cil.Cil.exp;
3. value : Cil.Cil.exp;
}
| SemWait of {
1. sem : Cil.Cil.exp;
2. try_ : bool;
3. timeout : Cil.Cil.exp option;
}
| SemPost of Cil.Cil.exp
| SemDestroy of 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;
3. n : 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;
}
| Bounded of {
1. exp : Cil.Cil.exp;
}
(*
Used to check for bounds for termination analysis.
*)
| 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.

module MathPrintable : sig ... end

module MathLifted : sig ... end