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