package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install 

dune-project
 Dependency

goblint.in.tum.de Edit opam file Versions (11)

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. K
    Karoliine Holter
  6. M
    Michael Petter
  7. A
    Ali Rasim Kocal
  8. R
    Ralf Vogler
  9. K
    Kalmer Apinis
  10. 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.8.0.tbz
sha256=9175eec0143102243964e34a0786584fd590c60422009259c705a89a27f88de4
sha512=9d760007dd8d003cf596516444ed7acc7370fc3d446e75ac71b0176522c3baae090410762f9035e7aae4f6b0e394bf28bb5b1c08ca0476920b94aa919ef04f42

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 NS : sig ... end
module ThreadNodeLattice : sig ... end
module VI : sig ... end
module VarQuery = Goblint_constraint.VarQuery
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 ProtectionKind : sig ... end
module Protection : sig ... end

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

module AllocationLocation : sig ... end
type maybepublic = {
  1. global : CilType.Varinfo.t;
  2. kind : ProtectionKind.t;
  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. kind : ProtectionKind.t;
  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. kind : ProtectionKind.t;
  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. kind : ProtectionKind.t;
}
val compare_mustprotectedvars : mustprotectedvars -> mustprotectedvars -> Ppx_deriving_runtime.int
val hash_mustprotectedvars : mustprotectedvars -> int
type mustprotectinglocks = {
  1. global : CilType.Varinfo.t;
  2. kind : ProtectionKind.t;
}
val compare_mustprotectinglocks : mustprotectinglocks -> mustprotectinglocks -> Ppx_deriving_runtime.int
val hash_mustprotectinglocks : mustprotectinglocks -> 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
module YS : sig ... end
module CL : sig ... end
module LH : sig ... end
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
    (*

    Use via ThreadEscape.has_escaped.

    *)
  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
    (*

    Use via ThreadFlag.is_currently_multi and ThreadFlag.has_ever_been_multi.

    *)
  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 : AllocationLocation.t -> 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.FiniteMustThreadSet.t t
  41. | ThreadsJoinedCleanly : MustBool.t t
  42. | MustProtectedVars : mustprotectedvars -> VS.t t
  43. | MustProtectingLocks : mustprotectinglocks -> LockDomain.MustLockset.t t
  44. | Invariant : invariant_context -> Invariant.t t
  45. | InvariantGlobal : Obj.t -> Invariant.t t
    (*

    Argument must be of corresponding Spec.V.t.

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

    Argument must be of corresponding Spec.V.t.

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

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

    *)
  48. | MayAccessed : AccessDomain.EventSet.t t
  49. | MayBeTainted : AD.t t
  50. | MayBeModifiedSinceSetjmp : JmpBufDomain.BufferEntry.t -> VS.t t
  51. | MustTermLoop : GoblintCil.stmt -> MustBool.t t
  52. | MustTermAllLoops : MustBool.t t
  53. | IsEverMultiThreaded : MayBool.t t
  54. | TmpSpecial : Mval.Exp.t -> ML.t t
  55. | MaySignedOverflow : GoblintCil.exp -> MayBool.t t
  56. | GasExhausted : CilType.Fundec.t -> MustBool.t t
  57. | YamlEntryGlobal : Obj.t * YamlWitnessType.Task.t -> YS.t t
    (*

    YAML witness entries for a global unknown (Obj.t represents Spec.V.t) and YAML witness task.

    *)
  58. | GhostVarAvailable : Goblint_lib__.WitnessGhostVar.t -> MayBool.t t
  59. | InvariantGlobalNodes : NS.t t
    (*

    Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if witness.invariant.flow_insensitive-as is configured to do so).

    *)
  60. | DescendantThreads : ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t
  61. | CreationLockset : ThreadIdDomain.Thread.t -> CL.t t
  62. | MustlockHistory : LH.t t
  63. | TutorialEffectivelyLocal : GoblintCil.varinfo -> MustBool.t t
    (*

    Used in tutorial for effectively local variables.

    *)

GADT for queries with specific result type.

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

Container for explicitly polymorphic man.ask function out of man. To be used when passing entire man around seems inappropriate. Use Analyses.ask_of_man to convert man 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 Bool : Lattice.S with type t = bool) -> GoblintCil.Cil.binop -> ask -> GoblintCil.exp -> GoblintCil.exp -> Bool.t
val must_be_equal : ask -> GoblintCil.exp -> GoblintCil.exp -> MustBool.t

Backwards-compatibility for former MustBeEqual query.

val may_be_equal : ask -> GoblintCil.exp -> GoblintCil.exp -> MayBool.t

Backwards-compatibility for former MayBeEqual query.

val may_be_less : ask -> GoblintCil.exp -> GoblintCil.exp -> MayBool.t

Backwards-compatibility for former MayBeLess query.

module Set : sig ... end
module Hashtbl : sig ... end