package goblint

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

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
module PartAccessResult = Access.PartAccessResult
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 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
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
type mustbeprotectedby = {
  1. mutex : PreValueDomain.Addr.t;
  2. global : CilType.Varinfo.t;
  3. write : bool;
}
val compare_mustbeprotectedby : mustbeprotectedby -> mustbeprotectedby -> Ppx_deriving_runtime.int
type partaccess = {
  1. exp : CilType.Exp.t;
  2. var_opt : CilType.Varinfo.t option;
  3. write : bool;
}
val compare_partaccess : partaccess -> partaccess -> Ppx_deriving_runtime.int
type _ t =
  1. | EqualSet : Cil.exp -> ES.t t
  2. | MayPointTo : Cil.exp -> LS.t t
  3. | ReachableFrom : Cil.exp -> LS.t t
  4. | ReachableUkTypes : Cil.exp -> TS.t t
  5. | Regions : Cil.exp -> LS.t t
  6. | MayEscape : Cil.varinfo -> MayBool.t t
  7. | Priority : string -> ID.t t
  8. | MayBePublic : maybepublic -> MayBool.t t
  9. | MayBePublicWithout : maybepublicwithout -> MayBool.t t
  10. | MustBeProtectedBy : mustbeprotectedby -> MustBool.t t
  11. | CurrentLockset : LS.t t
  12. | MustBeAtomic : MustBool.t t
  13. | MustBeSingleThreaded : MustBool.t t
  14. | MustBeUniqueThread : MustBool.t t
  15. | CurrentThreadId : ThreadIdDomain.ThreadLifted.t t
  16. | MayBeThreadReturn : MayBool.t t
  17. | EvalFunvar : Cil.exp -> LS.t t
  18. | EvalInt : Cil.exp -> ID.t t
  19. | EvalStr : Cil.exp -> SD.t t
  20. | EvalLength : Cil.exp -> ID.t t
  21. | BlobSize : Cil.exp -> ID.t t
  22. | PrintFullState : Unit.t t
  23. | CondVars : Cil.exp -> ES.t t
  24. | PartAccess : partaccess -> PartAccessResult.t t
  25. | IterPrevVars : iterprevvar -> Unit.t t
  26. | IterVars : itervar -> Unit.t t
  27. | MustBeEqual : Cil.exp * Cil.exp -> MustBool.t t
  28. | MayBeEqual : Cil.exp * Cil.exp -> MayBool.t t
  29. | MayBeLess : Cil.exp * Cil.exp -> MayBool.t t
  30. | HeapVar : VI.t t
  31. | IsHeapVar : Cil.varinfo -> MayBool.t t
  32. | IsMultiple : Cil.varinfo -> MustBool.t t
  33. | EvalThread : Cil.exp -> ConcDomain.ThreadSet.t t
  34. | CreatedThreads : ConcDomain.ThreadSet.t t
  35. | MustJoinedThreads : ConcDomain.MustThreadSet.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
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