Module `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

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

global : CilType.Varinfo.t;
write : bool;

}

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

type maybepublicwithout = {

global : CilType.Varinfo.t;
write : bool;
without_mutex : PreValueDomain.Addr.t;

}

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

type mustbeprotectedby = {

mutex : PreValueDomain.Addr.t;
global : CilType.Varinfo.t;
write : bool;

}

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

type partaccess = {

exp : CilType.Exp.t;
var_opt : CilType.Varinfo.t option;
write : bool;

}

val compare_partaccess : partaccess -> partaccess -> Ppx_deriving_runtime.int

type _ t =

| EqualSet : Cil.exp -> ES.t t
| MayPointTo : Cil.exp -> LS.t t
| ReachableFrom : Cil.exp -> LS.t t
| ReachableUkTypes : Cil.exp -> TS.t t
| Regions : Cil.exp -> LS.t t
| MayEscape : Cil.varinfo -> MayBool.t t
| Priority : string -> ID.t t
| MayBePublic : maybepublic -> MayBool.t t
| MayBePublicWithout : maybepublicwithout -> MayBool.t t
| MustBeProtectedBy : mustbeprotectedby -> MustBool.t t
| CurrentLockset : LS.t t
| MustBeAtomic : MustBool.t t
| MustBeSingleThreaded : MustBool.t t
| MustBeUniqueThread : MustBool.t t
| CurrentThreadId : ThreadIdDomain.ThreadLifted.t t
| MayBeThreadReturn : MayBool.t t
| EvalFunvar : Cil.exp -> LS.t t
| EvalInt : Cil.exp -> ID.t t
| EvalStr : Cil.exp -> SD.t t
| EvalLength : Cil.exp -> ID.t t
| BlobSize : Cil.exp -> ID.t t
| PrintFullState : Unit.t t
| CondVars : Cil.exp -> ES.t t
| PartAccess : partaccess -> PartAccessResult.t t
| IterPrevVars : iterprevvar -> Unit.t t
| IterVars : itervar -> Unit.t t
| MustBeEqual : Cil.exp * Cil.exp -> MustBool.t t
| MayBeEqual : Cil.exp * Cil.exp -> MayBool.t t
| MayBeLess : Cil.exp * Cil.exp -> MayBool.t t
| HeapVar : VI.t t
| IsHeapVar : Cil.varinfo -> MayBool.t t
| IsMultiple : Cil.varinfo -> MustBool.t t
| EvalThread : Cil.exp -> ConcDomain.ThreadSet.t t
| CreatedThreads : ConcDomain.ThreadSet.t t
| MustJoinedThreads : ConcDomain.MustThreadSet.t t

GADT for queries with specific result type.

type 'a result = 'a

type ask = {

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 =

| Any : 'a t -> any_query

module Any : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Queries/index.html

Module `Queries`

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Queries/index.html

Module Queries

Module `Queries`