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.lib/Goblint_lib/Queries/index.html

Module Goblint_lib.Queries

Queries and their result lattices.

module VDQ = ValueDomainQueries
module ID = VDQ.ID
module LS = VDQ.LS
module TS : sig ... end
module ES : sig ... end
module VS : sig ... end
module ThreadNodeLattice : sig ... end
module VI : sig ... end
type iterprevvar = int -> (MyCFG.node * Obj.t * int) -> MyARG.inline_edge -> unit
type itervar = int -> unit
val compare_itervar : 'a -> 'b -> int
val compare_iterprevvar : 'a -> 'b -> int
module FlatYojson : sig ... end
module SD : Lattice.S with type t = [ `Bot | `Lifted of string | `Top ]
module AD = ValueDomain.AD
module MayBool = BoolDomain.MayBool
module MustBool = BoolDomain.MustBool
module Unit = Lattice.Unit
module Protection : sig ... end

Different notions of protection for a global variables g by a mutex m m protects g strongly if:

type maybepublic = {
  1. global : CilType.Varinfo.t;
  2. write : bool;
  3. protection : Protection.t;
}
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 : LockDomain.MustLock.t;
  4. protection : Protection.t;
}
val compare_maybepublicwithout : maybepublicwithout -> maybepublicwithout -> Ppx_deriving_runtime.int
val hash_maybepublicwithout : maybepublicwithout -> int
type mustbeprotectedby = {
  1. mutex : LockDomain.MustLock.t;
  2. global : CilType.Varinfo.t;
  3. write : bool;
  4. protection : Protection.t;
}
val compare_mustbeprotectedby : mustbeprotectedby -> mustbeprotectedby -> Ppx_deriving_runtime.int
val hash_mustbeprotectedby : mustbeprotectedby -> int
type mustprotectedvars = {
  1. mutex : LockDomain.MustLock.t;
  2. write : bool;
}
val compare_mustprotectedvars : mustprotectedvars -> mustprotectedvars -> Ppx_deriving_runtime.int
val hash_mustprotectedvars : mustprotectedvars -> int
type access =
  1. | Memory of {
    1. exp : CilType.Exp.t;
    2. var_opt : CilType.Varinfo.t option;
    3. kind : AccessKind.t;
    }
    (*

    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. lvals : Lval.Set.t;
}
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 -> AD.t t
  3. | ReachableFrom : GoblintCil.exp -> AD.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 : LockDomain.MustLockset.t t
  11. | MustBeAtomic : MustBool.t t
  12. | MustBeSingleThreaded : {
    1. since_start : bool;
    } -> MustBool.t t
  13. | MustBeUniqueThread : MustBool.t t
  14. | CurrentThreadId : ThreadIdDomain.ThreadLifted.t t
  15. | ThreadCreateIndexedNode : ThreadNodeLattice.t t
  16. | MayBeThreadReturn : MayBool.t t
  17. | EvalFunvar : GoblintCil.exp -> AD.t t
  18. | EvalInt : GoblintCil.exp -> ID.t t
  19. | EvalStr : GoblintCil.exp -> SD.t t
  20. | EvalLength : GoblintCil.exp -> ID.t t
  21. | EvalValue : GoblintCil.exp -> VD.t t
  22. | BlobSize : {
    1. exp : GoblintCil.Cil.exp;
    2. base_address : bool;
    } -> ID.t t
  23. | CondVars : GoblintCil.exp -> ES.t t
  24. | PartAccess : access -> Obj.t t
    (*

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

    *)
  25. | IterPrevVars : iterprevvar -> Unit.t t
  26. | IterVars : itervar -> Unit.t t
  27. | PathQuery : int * 'a t -> 'a t
    (*

    Query only one path under witness lifter.

    *)
  28. | DYojson : FlatYojson.t t
    (*

    Get local state Yojson of one path under PathQuery.

    *)
  29. | AllocVar : {
    1. on_stack : bool;
    } -> VI.t t
  30. | IsAllocVar : GoblintCil.varinfo -> MayBool.t t
  31. | IsHeapVar : GoblintCil.varinfo -> MayBool.t t
  32. | IsMultiple : GoblintCil.varinfo -> MustBool.t t
  33. | MutexType : Mval.Unit.t -> MutexAttrDomain.t t
  34. | EvalThread : GoblintCil.exp -> ConcDomain.ThreadSet.t t
  35. | EvalMutexAttr : GoblintCil.exp -> MutexAttrDomain.t t
  36. | EvalJumpBuf : GoblintCil.exp -> JmpBufDomain.JmpBufSet.t t
  37. | ActiveJumpBuf : JmpBufDomain.ActiveLongjmps.t t
  38. | ValidLongJmp : JmpBufDomain.JmpBufSet.t t
  39. | CreatedThreads : ConcDomain.ThreadSet.t t
  40. | MustJoinedThreads : ConcDomain.MustThreadSet.t t
  41. | ThreadsJoinedCleanly : MustBool.t t
  42. | MustProtectedVars : mustprotectedvars -> VS.t t
  43. | Invariant : invariant_context -> Invariant.t t
  44. | InvariantGlobal : Obj.t -> Invariant.t t
    (*

    Argument must be of corresponding Spec.V.t.

    *)
  45. | WarnGlobal : Obj.t -> Unit.t t
    (*

    Argument must be of corresponding Spec.V.t.

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

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

    *)
  47. | MayAccessed : AccessDomain.EventSet.t t
  48. | MayBeTainted : AD.t t
  49. | MayBeModifiedSinceSetjmp : JmpBufDomain.BufferEntry.t -> VS.t t
  50. | MustTermLoop : GoblintCil.stmt -> MustBool.t t
  51. | MustTermAllLoops : MustBool.t t
  52. | IsEverMultiThreaded : MayBool.t t
  53. | TmpSpecial : Mval.Exp.t -> ML.t t
  54. | MaySignedOverflow : GoblintCil.exp -> MayBool.t t
  55. | GasExhausted : MustBool.t 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 to_value_domain_ask : ask -> VDQ.t
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