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. R
    Ralf Vogler
  6. K
    Kalmer Apinis
  7. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>

Sources

goblint-2.1.0.tbz
sha256=bfc412ec2e447eaef6f4f83892e3511ebf305593cb00561c1406be3ae8bf48e9
sha512=5f2a162e5f36bffafc9836b0d18b5b2808cecfa6bf68f83bb7d1e8b9947ac74cf07776eb09274b4b29d55c897a45a10768f0d9ed25810cf6ba2409c525e4cd4d

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

Module Goblint_lib.LibraryDesc

module Cil = GoblintCil

Library function descriptor (specification).

module Access : sig ... end

Pointer argument access specification.

type math =
  1. | Nan of Cil.fkind * Cil.exp
  2. | Inf of Cil.fkind
  3. | Isfinite of Cil.exp
  4. | Isinf of Cil.exp
  5. | Isnan of Cil.exp
  6. | Isnormal of Cil.exp
  7. | Signbit of Cil.exp
  8. | Isgreater of Cil.exp * Cil.exp
  9. | Isgreaterequal of Cil.exp * Cil.exp
  10. | Isless of Cil.exp * Cil.exp
  11. | Islessequal of Cil.exp * Cil.exp
  12. | Islessgreater of Cil.exp * Cil.exp
  13. | Isunordered of Cil.exp * Cil.exp
  14. | Ceil of Cil.fkind * Cil.exp
  15. | Floor of Cil.fkind * Cil.exp
  16. | Fabs of Cil.fkind * Cil.exp
  17. | Fmax of Cil.fkind * Cil.exp * Cil.exp
  18. | Fmin of Cil.fkind * Cil.exp * Cil.exp
  19. | Acos of Cil.fkind * Cil.exp
  20. | Asin of Cil.fkind * Cil.exp
  21. | Atan of Cil.fkind * Cil.exp
  22. | Atan2 of Cil.fkind * Cil.exp * Cil.exp
  23. | Cos of Cil.fkind * Cil.exp
  24. | Sin of Cil.fkind * Cil.exp
  25. | Tan of Cil.fkind * Cil.exp
type special =
  1. | Malloc of Cil.exp
  2. | Calloc of {
    1. count : Cil.exp;
    2. size : Cil.exp;
    }
  3. | Realloc of {
    1. ptr : Cil.exp;
    2. size : Cil.exp;
    }
  4. | Assert of {
    1. exp : Cil.exp;
    2. check : bool;
    3. refine : bool;
    }
  5. | Lock of {
    1. lock : Cil.exp;
    2. try_ : bool;
    3. write : bool;
    4. return_on_success : bool;
    }
  6. | Unlock of Cil.exp
  7. | ThreadCreate of {
    1. thread : Cil.exp;
    2. start_routine : Cil.exp;
    3. arg : Cil.exp;
    }
  8. | ThreadJoin of {
    1. thread : Cil.exp;
    2. ret_var : Cil.exp;
    }
  9. | ThreadExit of {
    1. ret_val : Cil.exp;
    }
  10. | Signal of Cil.exp
  11. | Broadcast of Cil.exp
  12. | Wait of {
    1. cond : Cil.exp;
    2. mutex : Cil.exp;
    }
  13. | TimedWait of {
    1. cond : Cil.exp;
    2. mutex : Cil.exp;
    3. abstime : Cil.exp;
      (*

      Unused

      *)
    }
  14. | Math of {
    1. fun_args : math;
    }
  15. | Memset of {
    1. dest : Cil.exp;
    2. ch : Cil.exp;
    3. count : Cil.exp;
    }
  16. | Bzero of {
    1. dest : Cil.exp;
    2. count : Cil.exp;
    }
  17. | Memcpy of {
    1. dest : Cil.exp;
    2. src : Cil.exp;
    }
  18. | Strcpy of {
    1. dest : Cil.exp;
    2. src : Cil.exp;
    }
  19. | Abort
  20. | Identity of Cil.exp
    (*

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

    *)
  21. | 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.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 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