Module CreationLockset.Spec

include module type of struct include Analyses.IdentityUnitContextsSpec end
include module type of struct include Analyses.IdentitySpec end
include module type of struct include Analyses.DefaultSpec end
module P = Analyses.EmptyP
type marshal = unit
val init : 'a -> unit
val finalize : unit -> unit
val vdecl : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'a
val asm : ('a, 'b, 'c, 'd) Analyses.man -> 'a
val skip : ('a, 'b, 'c, 'd) Analyses.man -> 'a
val morphstate : 'a -> 'b -> 'b
val sync : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'a
val paths_as_set : ('a, 'b, 'c, 'd) Analyses.man -> 'a list
val assign : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.lval -> GoblintCil.exp -> 'a
val branch : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.exp -> bool -> 'a
val body : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.fundec -> 'a
val return : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.exp option -> GoblintCil.fundec -> 'a
val enter : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.lval option -> GoblintCil.fundec -> GoblintCil.exp list -> ('a * 'a) list
val combine_env : 'a -> GoblintCil.lval option -> 'b -> GoblintCil.fundec -> GoblintCil.exp list -> 'c -> 'd -> Queries.ask -> 'd
val combine_assign : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.lval option -> 'e -> GoblintCil.fundec -> GoblintCil.exp list -> 'f -> 'g -> Queries.ask -> 'a
val special : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> 'a
val threadenter : ('a, 'b, 'c, 'd) Analyses.man -> multiple:'e -> 'f -> 'g -> 'h -> 'a list
module C = Printable.Unit
val context : 'a -> 'b -> 'c -> unit
val startcontext : unit -> unit
module D = Lattice.Unit
module V = Analyses.TIDV
module G = Queries.CL
val name : unit -> string
val startstate : 'a -> unit
val exitstate : 'a -> unit
val contribute_locks : ('a, 'b, 'c, 'd) Analyses.man -> 'b -> 'd -> unit

register a global contribution: global.child_tid \supseteq to_contribute

  • parameter man

    man at program point

  • parameter to_contribute

    new edges from child_tid to ego thread to register

  • parameter child_tid
val threadspawn : ('a, G.t, 'b, TIDs.elt) Analyses.man -> multiple:'c -> 'd -> 'e -> 'f -> ('g, 'h, 'i, 'j) Analyses.man -> unit
val unlock : ('a, G.t, 'b, TIDs.elt) Analyses.man -> G.key -> TIDs.t -> Lockset.elt -> unit

handle unlock of mutex lock

val unknown_unlock : ('a, G.t, 'b, TIDs.elt) Analyses.man -> G.key -> TIDs.t -> unit

handle unlock of an unknown mutex. Assumes that any mutex could have been unlocked

val event : ('a, G.t, 'b, TIDs.elt) Analyses.man -> Events.t -> 'c -> unit
module A : sig ... end