package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

Dune Dependency

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

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.0.1.tbz
sha256=dba2b664c7c125687e708e871d83fbfb6ba6d9ee98d235b4850d9a238caa84de
sha512=529987cde39691ad9e955000a3603e89c1c8cf14ed5e8b4cd3a7fc26e47d016aff571b472e2329725133c46f8d0cb45a05b88994eeffaa221a4d31b4c543adcd

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

Module Goblint_lib.Queries

Structures for the querying subsystem.

module GU = Goblintutil
module ID : sig ... end
module LS : sig ... end
module TS : sig ... end
module ES : sig ... end
module VI : sig ... end
type iterprevvar = int -> (MyCFG.node * Stdlib.Obj.t * int) -> MyARG.inline_edge -> unit
type itervar = int -> unit
val compare_itervar : 'a -> 'b -> int
val compare_iterprevvar : 'a -> 'b -> int
module SD = Basetype.Strings
module MayBool = BoolDomain.MayBool
module MustBool = BoolDomain.MustBool
module Unit = Lattice.Unit
type maybepublic = {
  1. global : CilType.Varinfo.t;
  2. write : bool;
}
val compare_maybepublic : maybepublic -> maybepublic -> Ppx_deriving_runtime.int
val hash_maybepublic : maybepublic -> int
type maybepublicwithout = {
  1. global : CilType.Varinfo.t;
  2. write : bool;
  3. without_mutex : PreValueDomain.Addr.t;
}
val compare_maybepublicwithout : maybepublicwithout -> maybepublicwithout -> Ppx_deriving_runtime.int
val hash_maybepublicwithout : maybepublicwithout -> int
type mustbeprotectedby = {
  1. mutex : PreValueDomain.Addr.t;
  2. global : CilType.Varinfo.t;
  3. write : bool;
}
val compare_mustbeprotectedby : mustbeprotectedby -> mustbeprotectedby -> Ppx_deriving_runtime.int
val hash_mustbeprotectedby : mustbeprotectedby -> int
type memory_access = {
  1. exp : CilType.Exp.t;
  2. var_opt : CilType.Varinfo.t option;
  3. kind : AccessKind.t;
}
val compare_memory_access : memory_access -> memory_access -> Ppx_deriving_runtime.int
val hash_memory_access : memory_access -> int
type access =
  1. | Memory of memory_access
    (*

    Memory location access (race).

    *)
  2. | Point
    (*

    Program point and state access (MHP), independent of memory location.

    *)
val compare_access : access -> access -> Ppx_deriving_runtime.int
val hash_access : access -> int
type invariant_context = Invariant.context = {
  1. path : int option;
  2. lval : CilType.Lval.t option;
}
val compare_invariant_context : invariant_context -> invariant_context -> Ppx_deriving_runtime.int
val hash_invariant_context : invariant_context -> int
type _ t =
  1. | EqualSet : GoblintCil.exp -> ES.t t
  2. | MayPointTo : GoblintCil.exp -> LS.t t
  3. | ReachableFrom : GoblintCil.exp -> LS.t t
  4. | ReachableUkTypes : GoblintCil.exp -> TS.t t
  5. | Regions : GoblintCil.exp -> LS.t t
  6. | MayEscape : GoblintCil.varinfo -> MayBool.t t
  7. | MayBePublic : maybepublic -> MayBool.t t
  8. | MayBePublicWithout : maybepublicwithout -> MayBool.t t
  9. | MustBeProtectedBy : mustbeprotectedby -> MustBool.t t
  10. | MustLockset : LS.t t
  11. | MustBeAtomic : MustBool.t t
  12. | MustBeSingleThreaded : MustBool.t t
  13. | MustBeUniqueThread : MustBool.t t
  14. | CurrentThreadId : ThreadIdDomain.ThreadLifted.t t
  15. | MayBeThreadReturn : MayBool.t t
  16. | EvalFunvar : GoblintCil.exp -> LS.t t
  17. | EvalInt : GoblintCil.exp -> ID.t t
  18. | EvalStr : GoblintCil.exp -> SD.t t
  19. | EvalLength : GoblintCil.exp -> ID.t t
  20. | BlobSize : GoblintCil.exp -> ID.t t
  21. | CondVars : GoblintCil.exp -> ES.t t
  22. | PartAccess : access -> Stdlib.Obj.t t
    (*

    Only queried by access and deadlock analysis. Obj.t represents MCPAccess.A.t, needed to break dependency cycle.

    *)
  23. | IterPrevVars : iterprevvar -> Unit.t t
  24. | IterVars : itervar -> Unit.t t
  25. | HeapVar : VI.t t
  26. | IsHeapVar : GoblintCil.varinfo -> MayBool.t t
  27. | IsMultiple : GoblintCil.varinfo -> MustBool.t t
  28. | EvalThread : GoblintCil.exp -> ConcDomain.ThreadSet.t t
  29. | CreatedThreads : ConcDomain.ThreadSet.t t
  30. | MustJoinedThreads : ConcDomain.MustThreadSet.t t
  31. | Invariant : invariant_context -> Invariant.t t
  32. | WarnGlobal : Stdlib.Obj.t -> Unit.t t
    (*

    Argument must be of corresponding Spec.V.t.

    *)
  33. | IterSysVars : VarQuery.t * Stdlib.Obj.t VarQuery.f -> Unit.t t
    (*

    iter_vars for Constraints.FromSpec. Obj.t represents Spec.V.t.

    *)

GADT for queries with specific result type.

type 'a result = 'a
type ask = {
  1. f : 'a. 'a t -> 'a result;
}

Container for explicitly polymorphic ctx.ask function out of ctx. To be used when passing entire ctx around seems inappropriate. Use Analyses.ask_of_ctx to convert ctx to ask.

module Result : sig ... end
type any_query =
  1. | Any : 'a t -> any_query
module Any : sig ... end
val eval_int_binop : (module Lattice.S with type t = bool) -> GoblintCil__.Cil.binop -> ask -> GoblintCil.exp -> GoblintCil.exp -> bool
val must_be_equal : ask -> GoblintCil.exp -> GoblintCil.exp -> bool

Backwards-compatibility for former MustBeEqual query.

val may_be_equal : ask -> GoblintCil.exp -> GoblintCil.exp -> bool

Backwards-compatibility for former MayBeEqual query.

val may_be_less : ask -> GoblintCil.exp -> GoblintCil.exp -> bool

Backwards-compatibility for former MayBeLess query.

module Set : sig ... end
module Hashtbl : 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