package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 * 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 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 -> Stdlib.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 : Stdlib.Obj.t -> Invariant.t t
    (*

    Argument must be of corresponding Spec.V.t.

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

    Argument must be of corresponding Spec.V.t.

    *)
  46. | IterSysVars : VarQuery.t * Stdlib.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
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