package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6
sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af
doc/goblint.lib/Goblint_lib/Queries/index.html
Module Goblint_lib.Queries
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 NFL = WrapperFunctionAnalysis0.NodeFlatLattice
module TC = WrapperFunctionAnalysis0.ThreadCreateUniqueCount
module ThreadNodeLattice : sig ... end
module ML = LibraryDesc.MathLifted
module VI : sig ... end
type iterprevvar =
int ->
(MyCFG.node * Stdlib.Obj.t * int) ->
MyARG.inline_edge ->
unit
module FlatYojson : sig ... end
module VD = ValueDomain.Compound
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:
val compare_maybepublic :
maybepublic ->
maybepublic ->
Ppx_deriving_runtime.int
val hash_maybepublic : maybepublic -> int
type maybepublicwithout = {
global : CilType.Varinfo.t;
write : bool;
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;
write : bool;
protection : Protection.t;
}
val compare_mustbeprotectedby :
mustbeprotectedby ->
mustbeprotectedby ->
Ppx_deriving_runtime.int
val hash_mustbeprotectedby : mustbeprotectedby -> int
val compare_mustprotectedvars :
mustprotectedvars ->
mustprotectedvars ->
Ppx_deriving_runtime.int
val hash_mustprotectedvars : mustprotectedvars -> int
type access =
| Memory of {
exp : CilType.Exp.t;
var_opt : CilType.Varinfo.t option;
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
val compare_invariant_context :
invariant_context ->
invariant_context ->
Ppx_deriving_runtime.int
val hash_invariant_context : invariant_context -> int
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 : {
} -> 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 : {
exp : GoblintCil.Cil.exp;
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
representsMCPAccess.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 : {
} -> 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
| 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
forConstraints.FromSpec
.Obj.t
representsSpec.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 : MustBool.t t
GADT for queries with specific result type.
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
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