package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install 

dune-project
 Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (9)

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. K
    Karoliine Holter
  6. R
    Ralf Vogler
  7. K
    Kalmer Apinis
  8. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>
  3. K
    Karoliine Holter <karoliine.holter@ut.ee>

Sources

goblint-2.4.0.tbz
sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6
sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af

doc/goblint.library/LibraryDesc/index.html

Module LibraryDescSource

Library function descriptor (specification).

Sourcemodule Cil = GoblintCil

Pointer argument access specification.

Sourcemodule Access : sig ... end

Pointer argument access specification.

Sourceval compare_math : math -> math -> Ppx_deriving_runtime.int
Sourceval hash_math : math -> int
Sourcetype 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;
    4. multiple : bool;
    }
  10. | ThreadJoin of {
    1. thread : Cil.Cil.exp;
    2. ret_var : Cil.Cil.exp;
    }
  11. | ThreadExit of {
    1. ret_val : Cil.Cil.exp;
    }
  12. | Globalize of Cil.Cil.exp
  13. | Signal of Cil.Cil.exp
  14. | Broadcast of Cil.Cil.exp
  15. | MutexAttrSetType of {
    1. attr : Cil.Cil.exp;
    2. typ : Cil.Cil.exp;
    }
  16. | MutexInit of {
    1. mutex : Cil.Cil.exp;
    2. attr : Cil.Cil.exp;
    }
  17. | SemInit of {
    1. sem : Cil.Cil.exp;
    2. pshared : Cil.Cil.exp;
    3. value : Cil.Cil.exp;
    }
  18. | SemWait of {
    1. sem : Cil.Cil.exp;
    2. try_ : bool;
    3. timeout : Cil.Cil.exp option;
    }
  19. | SemPost of Cil.Cil.exp
  20. | SemDestroy of Cil.Cil.exp
  21. | Wait of {
    1. cond : Cil.Cil.exp;
    2. mutex : Cil.Cil.exp;
    }
  22. | TimedWait of {
    1. cond : Cil.Cil.exp;
    2. mutex : Cil.Cil.exp;
    3. abstime : Cil.Cil.exp;
      (*

      Unused

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

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

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

    Used to check for bounds for termination analysis.

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

    Anything not belonging to other types.

    *)

Type of special function, or Unknown.

Sourcemodule Accesses : sig ... end

Pointer arguments access specification.

Sourcetype 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.

Sourcetype 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.

Sourcemodule MathPrintable : sig ... end
Sourcemodule MathLifted : sig ... end