Module Goblint_lib.Queries

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
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
val hash_maybepublic : maybepublic -> 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
val hash_maybepublicwithout : maybepublicwithout -> 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
val hash_mustbeprotectedby : mustbeprotectedby -> int
type memory_access = {
  1. exp : CilType.Exp.t;
  2. var_opt : CilType.Varinfo.t option;
  3. kind : AccessKind.t;
}
val compare_memory_access : memory_access -> memory_access -> Ppx_deriving_runtime.int
val hash_memory_access : memory_access -> int
type access =
  1. | Memory of memory_access
    (*

    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. lval : CilType.Lval.t option;
}
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 -> LS.t t
  3. | ReachableFrom : GoblintCil.exp -> LS.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 : LS.t t
  11. | MustBeAtomic : MustBool.t t
  12. | MustBeSingleThreaded : MustBool.t t
  13. | MustBeUniqueThread : MustBool.t t
  14. | CurrentThreadId : ThreadIdDomain.ThreadLifted.t t
  15. | MayBeThreadReturn : MayBool.t t
  16. | EvalFunvar : GoblintCil.exp -> LS.t t
  17. | EvalInt : GoblintCil.exp -> ID.t t
  18. | EvalStr : GoblintCil.exp -> SD.t t
  19. | EvalLength : GoblintCil.exp -> ID.t t
  20. | BlobSize : GoblintCil.exp -> ID.t t
  21. | CondVars : GoblintCil.exp -> ES.t t
  22. | PartAccess : access -> Obj.t t
    (*

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

    *)
  23. | IterPrevVars : iterprevvar -> Unit.t t
  24. | IterVars : itervar -> Unit.t t
  25. | HeapVar : VI.t t
  26. | IsHeapVar : GoblintCil.varinfo -> MayBool.t t
  27. | IsMultiple : GoblintCil.varinfo -> MustBool.t t
  28. | EvalThread : GoblintCil.exp -> ConcDomain.ThreadSet.t t
  29. | CreatedThreads : ConcDomain.ThreadSet.t t
  30. | MustJoinedThreads : ConcDomain.MustThreadSet.t t
  31. | Invariant : invariant_context -> Invariant.t t
  32. | WarnGlobal : Obj.t -> Unit.t t
    (*

    Argument must be of corresponding Spec.V.t.

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

    iter_vars for Constraints.FromSpec. Obj.t represents Spec.V.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 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