Module `ThreadId.Spec`

include module type of struct include Analyses.IdentitySpec end

include module type of struct include Analyses.DefaultSpec end

module G = Lattice.Unit

module V = Analyses.EmptyV

val vdecl : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'a

val asm : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a

val skip : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a

val event : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'f -> 'a

val sync : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'a

val paths_as_set : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a list

val assign : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.lval ->
  GoblintCil.exp ->
  'a

val branch : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.exp -> bool -> 'a

val body : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.fundec -> 'a

val return : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.exp option ->
  GoblintCil.fundec ->
  'a

val combine_assign : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.lval option ->
  'e ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  'f ->
  'g ->
  Queries.ask ->
  'a

val special : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  'a

module N : sig ... end

module TD = Thread.D

module D : sig ... end

Uniqueness Counter * TID * (All thread creates of current thread * All thread creates of the current function and its callees)

module C = D

module P : sig ... end

val tids : (Thread.t, unit) Batteries.Hashtbl.t Stdlib.ref

val name : unit -> string

val context : 'a -> ('b * 'c * (TD.t * TD.t)) -> 'b * 'c * (TD.t * TD.t)

val startstate : 'a -> [> `Bot ] * [> `Bot ] * (TD.t * TD.t)

val exitstate : 
  GoblintCil.varinfo ->
  [> `Bot ] * [> `Lifted of Thread.t ] * (TD.t * TD.t)

val morphstate : 
  GoblintCil.varinfo ->
  'a ->
  [> `Bot ] * [> `Lifted of Thread.t ] * (TD.t * TD.t)

val create_tid : 
  ('a * [> `Lifted of Thread.t ] * (Thread.D.t * 'b)) ->
  (Node.t * int option) ->
  GoblintCil.varinfo ->
  [> `Lifted of Thread.t ] list

val is_unique : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  BoolDomain.MustBool.t Queries.result

val enter : 
  ('a * 'b * ('c * 'd), 'e, 'f, 'g) Analyses.ctx ->
  'h ->
  'i ->
  'j ->
  (('a * 'b * ('c * 'd)) * ('a * 'b * ('c * TD.t))) list

val combine_env : 
  ('a * 'b * (TD.t * TD.t), 'c, 'd, 'e) Analyses.ctx ->
  'f ->
  'g ->
  'h ->
  'i ->
  'j ->
  ('k * 'l * (TD.t * TD.t)) ->
  'm ->
  'k * 'l * (TD.t * TD.t)

val created : 
  ('a * [> `Lifted of Thread.t ] * (Thread.D.t * 'b)) ->
  ConcDomain.ThreadSet.t

val query : (D.t, 'b, 'c, 'd) Analyses.ctx -> 'a Queries.t -> 'a Queries.result

module A : sig ... end

val access : ('a * 'b * 'c, 'd, 'e, 'f) Analyses.ctx -> 'g -> 'b option

val indexed_node_for_ctx : ('a, 'b, 'c, 'd) Analyses.ctx -> Node.t * int option

get the node that identifies the current context, possibly that of a wrapper function

val threadenter : 
  ('a * [> `Lifted of Thread.t ] * (Thread.D.t * 'b), 'c, 'd, 'e) Analyses.ctx ->
  'f ->
  GoblintCil.varinfo ->
  'g ->
  D.t list

val threadspawn : 
  ('a * 'b * (Thread.D.t * Thread.D.t), 'c, 'd, 'e) Analyses.ctx ->
  'f ->
  'g ->
  'h ->
  ([> `Lifted of GoblintCil.varinfo * Node.t * int option ] * 'i * 'j,
    'k,
    'l,
    'm)
    Analyses.ctx ->
  'a * 'b * (Thread.D.t * Thread.D.t)

type marshal = (Thread.t, unit) Batteries.Hashtbl.t

val init : marshal option -> unit

val print_tid_info : unit -> unit

val finalize : unit -> (Thread.t, unit) Batteries.Hashtbl.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/ThreadId/Spec/index.html

Module `ThreadId.Spec`

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/ThreadId/Spec/index.html

Module ThreadId.Spec

Module `ThreadId.Spec`