Queries (goblint.Goblint

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 NFL = WrapperFunctionAnalysis0.NodeFlatLattice

module TC = WrapperFunctionAnalysis0.ThreadCreateUniqueCount

module ThreadNodeLattice : sig ... end

module ML = LibraryDesc.MathLifted

module VI : sig ... end

module VarQuery = Goblint_constraint.VarQuery

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 VD = ValueDomain.Compound

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 = {

global : CilType.Varinfo.t;
kind : ProtectionKind.t;
protection : Protection.t;

}

val compare_maybepublic : 
  maybepublic ->
  maybepublic ->
  Ppx_deriving_runtime.int

val hash_maybepublic : maybepublic -> int

type maybepublicwithout = {

global : CilType.Varinfo.t;
kind : ProtectionKind.t;
without_mutex : LockDomain.MustLock.t;
protection : Protection.t;

}

val compare_maybepublicwithout : 
  maybepublicwithout ->
  maybepublicwithout ->
  Ppx_deriving_runtime.int

val hash_maybepublicwithout : maybepublicwithout -> int

type mustbeprotectedby = {

mutex : LockDomain.MustLock.t;
global : CilType.Varinfo.t;
kind : ProtectionKind.t;
protection : Protection.t;

}

val compare_mustbeprotectedby : 
  mustbeprotectedby ->
  mustbeprotectedby ->
  Ppx_deriving_runtime.int

val hash_mustbeprotectedby : mustbeprotectedby -> int

type mustprotectedvars = {

mutex : LockDomain.MustLock.t;
kind : ProtectionKind.t;

}

val compare_mustprotectedvars : 
  mustprotectedvars ->
  mustprotectedvars ->
  Ppx_deriving_runtime.int

val hash_mustprotectedvars : mustprotectedvars -> int

type mustprotectinglocks = {

global : CilType.Varinfo.t;
kind : ProtectionKind.t;

}

val compare_mustprotectinglocks : 
  mustprotectinglocks ->
  mustprotectinglocks ->
  Ppx_deriving_runtime.int

val hash_mustprotectinglocks : mustprotectinglocks -> int

type access =

| Memory of {
1. exp : CilType.Exp.t;
2. var_opt : CilType.Varinfo.t option;
3. kind : AccessKind.t;
}
(*
Memory location access (race).
*)
| 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 = {

path : int option;
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

type _ t =

| EqualSet : GoblintCil.exp -> ES.t t
| MayPointTo : GoblintCil.exp -> AD.t t
| ReachableFrom : GoblintCil.exp -> AD.t t
| ReachableUkTypes : GoblintCil.exp -> TS.t t
| Regions : GoblintCil.exp -> LS.t t
| MayEscape : GoblintCil.varinfo -> MayBool.t t
| MayBePublic : maybepublic -> MayBool.t t
| MayBePublicWithout : maybepublicwithout -> MayBool.t t
| MustBeProtectedBy : mustbeprotectedby -> MustBool.t t
| MustLockset : LockDomain.MustLockset.t t
| MustBeAtomic : MustBool.t t
| MustBeSingleThreaded : {
1. since_start : bool;
} -> MustBool.t t
| MustBeUniqueThread : MustBool.t t
| CurrentThreadId : ThreadIdDomain.ThreadLifted.t t
| ThreadCreateIndexedNode : ThreadNodeLattice.t t
| MayBeThreadReturn : MayBool.t t
| EvalFunvar : GoblintCil.exp -> AD.t t
| EvalInt : GoblintCil.exp -> ID.t t
| EvalStr : GoblintCil.exp -> SD.t t
| EvalLength : GoblintCil.exp -> ID.t t
| EvalValue : GoblintCil.exp -> VD.t t
| BlobSize : {
1. exp : GoblintCil.Cil.exp;
2. base_address : bool;
} -> ID.t t
| CondVars : GoblintCil.exp -> ES.t t
| PartAccess : access -> Stdlib.Obj.t t
(*
Only queried by access and deadlock analysis. Obj.t represents MCPAccess.A.t, needed to break dependency cycle.
*)
| IterPrevVars : iterprevvar -> Unit.t t
| IterVars : itervar -> Unit.t t
| PathQuery : int * 'a t -> 'a t
(*
Query only one path under witness lifter.
*)
| DYojson : FlatYojson.t t
(*
Get local state Yojson of one path under PathQuery.
*)
| AllocVar : AllocationLocation.t -> VI.t t
| IsAllocVar : GoblintCil.varinfo -> MayBool.t t
| IsHeapVar : GoblintCil.varinfo -> MayBool.t t
| IsMultiple : GoblintCil.varinfo -> MustBool.t t
| MutexType : Mval.Unit.t -> MutexAttrDomain.t t
| EvalThread : GoblintCil.exp -> ConcDomain.ThreadSet.t t
| EvalMutexAttr : GoblintCil.exp -> MutexAttrDomain.t t
| EvalJumpBuf : GoblintCil.exp -> JmpBufDomain.JmpBufSet.t t
| ActiveJumpBuf : JmpBufDomain.ActiveLongjmps.t t
| ValidLongJmp : JmpBufDomain.JmpBufSet.t t
| CreatedThreads : ConcDomain.ThreadSet.t t
| MustJoinedThreads : ConcDomain.MustThreadSet.t t
| ThreadsJoinedCleanly : MustBool.t t
| MustProtectedVars : mustprotectedvars -> VS.t t
| MustProtectingLocks : mustprotectinglocks -> LockDomain.MustLockset.t t
| Invariant : invariant_context -> Invariant.t t
| InvariantGlobal : Stdlib.Obj.t -> Invariant.t t
(*
Argument must be of corresponding Spec.V.t.
*)
| WarnGlobal : Stdlib.Obj.t -> Unit.t t
(*
Argument must be of corresponding Spec.V.t.
*)
| IterSysVars : VarQuery.t * Stdlib.Obj.t VarQuery.f -> Unit.t t
(*
iter_vars for Constraints.FromSpec. Obj.t represents Spec.V.t.
*)
| MayAccessed : AccessDomain.EventSet.t t
| MayBeTainted : AD.t t
| MayBeModifiedSinceSetjmp : JmpBufDomain.BufferEntry.t -> VS.t t
| MustTermLoop : GoblintCil.stmt -> MustBool.t t
| MustTermAllLoops : MustBool.t t
| IsEverMultiThreaded : MayBool.t t
| TmpSpecial : Mval.Exp.t -> ML.t t
| MaySignedOverflow : GoblintCil.exp -> MayBool.t t
| GasExhausted : CilType.Fundec.t -> MustBool.t t
| YamlEntryGlobal : Stdlib.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.
*)
| GhostVarAvailable : Goblint_lib__.WitnessGhostVar.t -> MayBool.t t
| 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).
*)

GADT for queries with specific result type.

type 'a result = 'a

type ask = {

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 =

| 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.

val eval_bool : ask -> GoblintCil.exp -> BoolDomain.FlatBool.t

module Set : sig ... end

module Hashtbl : sig ... end