package goblint

  1. Overview
  2. Docs
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.

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 =
  1. | Alloca of Cil.Cil.exp
  2. | Malloc of Cil.Cil.exp
  3. | Calloc of {
    1. count : Cil.Cil.exp;
    2. size : Cil.Cil.exp;
    }
  4. | Realloc of {
    1. ptr : Cil.Cil.exp;
    2. size : Cil.Cil.exp;
    }
  5. | Free of Cil.Cil.exp
  6. | Assert of {
    1. exp : Cil.Cil.exp;
    2. check : bool;
    3. refine : bool;
    }
  7. | Lock of {
    1. lock : Cil.Cil.exp;
    2. try_ : bool;
    3. write : bool;
    4. return_on_success : bool;
    }
  8. | Unlock of Cil.Cil.exp
  9. | ThreadCreate of {
    1. thread : Cil.Cil.exp;
    2. start_routine : Cil.Cil.exp;
    3. arg : Cil.Cil.exp;
    }
  10. | ThreadJoin of {
    1. thread : Cil.Cil.exp;
    2. ret_var : Cil.Cil.exp;
    }
  11. | ThreadExit of {
    1. ret_val : Cil.Cil.exp;
    }
  12. | Signal of Cil.Cil.exp
  13. | Broadcast of Cil.Cil.exp
  14. | MutexAttrSetType of {
    1. attr : Cil.Cil.exp;
    2. typ : Cil.Cil.exp;
    }
  15. | MutexInit of {
    1. mutex : Cil.Cil.exp;
    2. attr : Cil.Cil.exp;
    }
  16. | SemInit of {
    1. sem : Cil.Cil.exp;
    2. pshared : Cil.Cil.exp;
    3. value : Cil.Cil.exp;
    }
  17. | SemWait of {
    1. sem : Cil.Cil.exp;
    2. try_ : bool;
    3. timeout : Cil.Cil.exp option;
    }
  18. | SemPost of Cil.Cil.exp
  19. | SemDestroy of Cil.Cil.exp
  20. | Wait of {
    1. cond : Cil.Cil.exp;
    2. mutex : Cil.Cil.exp;
    }
  21. | TimedWait of {
    1. cond : Cil.Cil.exp;
    2. mutex : Cil.Cil.exp;
    3. abstime : Cil.Cil.exp;
      (*

      Unused

      *)
    }
  22. | Math of {
    1. fun_args : math;
    }
  23. | Memset of {
    1. dest : Cil.Cil.exp;
    2. ch : Cil.Cil.exp;
    3. count : Cil.Cil.exp;
    }
  24. | Bzero of {
    1. dest : Cil.Cil.exp;
    2. count : Cil.Cil.exp;
    }
  25. | Memcpy of {
    1. dest : Cil.Cil.exp;
    2. src : Cil.Cil.exp;
    3. n : Cil.Cil.exp;
    }
  26. | Strcpy of {
    1. dest : Cil.Cil.exp;
    2. src : Cil.Cil.exp;
    3. n : Cil.Cil.exp option;
    }
  27. | Strcat of {
    1. dest : Cil.Cil.exp;
    2. src : Cil.Cil.exp;
    3. n : Cil.Cil.exp option;
    }
  28. | Strlen of Cil.Cil.exp
  29. | Strstr of {
    1. haystack : Cil.Cil.exp;
    2. needle : Cil.Cil.exp;
    }
  30. | Strcmp of {
    1. s1 : Cil.Cil.exp;
    2. s2 : Cil.Cil.exp;
    3. n : Cil.Cil.exp option;
    }
  31. | Abort
  32. | Identity of Cil.Cil.exp
    (*

    Identity function. Some compiler optimization annotation functions map to this.

    *)
  33. | Setjmp of {
    1. env : Cil.Cil.exp;
    }
  34. | Longjmp of {
    1. env : Cil.Cil.exp;
    2. value : Cil.Cil.exp;
    }
  35. | Bounded of {
    1. exp : Cil.Cil.exp;
    }
    (*

    Used to check for bounds for termination analysis.

    *)
  36. | Rand
  37. | Unknown
    (*

    Anything not belonging to other types.

    *)

Type of special function, or Unknown.

module Accesses : sig ... end

Pointer arguments access specification.

type attr =
  1. | ThreadUnsafe
    (*

    Function is not thread-safe to call, e.g. due to its own internal (global) state.

    *)
  2. | InvalidateGlobals
    (*

    Function invalidates all globals when called.

    *)

Function attribute.

type t = {
  1. special : Cil.Cil.exp list -> special;
    (*

    Conversion to special using arguments.

    *)
  2. accs : Accesses.t;
    (*

    Pointer arguments access specification.

    *)
  3. attrs : attr list;
    (*

    Attributes of function.

    *)
}

Library function descriptor.

val of_old : ?attrs:attr list -> Accesses.old -> t
module MathPrintable : sig ... end
module MathLifted : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct