Spec (goblint.Goblint_lib.ThreadId.Spec)

include module type of struct include Analyses.IdentitySpec end

include module type of struct include Analyses.DefaultSpec end

Relatively safe default implementations of some boring Spec functions.

module G = Lattice.Unit

module V = Analyses.EmptyV

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

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

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

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

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

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

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

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

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

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

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

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

module N : sig ... end

module TD = Thread.D

module Created : sig ... end

module D : sig ... end

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

include sig ... end

module C : sig ... end

val startcontext : unit -> D.t

module P : sig ... end

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

val name : unit -> string

val context : 'a -> 'b -> ('c * 'd * (TD.t * TD.t)) -> 'c * 'd * (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 : 
  ?multiple:bool ->
  ('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)) * ('k * 'l * ('m * 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 ->
  'a0 Queries.result

module A : sig ... end

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

val indexed_node_for_ctx : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  Node.t * WrapperFunctionAnalysis0.ThreadCreateUniqueCount.t 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 ->
  multiple:bool ->
  'f ->
  GoblintCil.varinfo ->
  'g ->
  D.t list

val threadspawn : 
  ('a * 'b * (Thread.D.t * Thread.D.t), 'c, 'd, 'e) Analyses.ctx ->
  multiple:bool ->
  'f ->
  'g ->
  'h ->
  ([> `Lifted of GoblintCil.varinfo * Node.t * int option ] * 'i * 'j,
    'k,
    'l,
    'm)
    Analyses.ctx ->
  'n * 'o * (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