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 query : 'b -> 'a Queries.t -> '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 : sig ... end
module G : sig ... end
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 must_ancestor_descendants_closure : ('a, 'b, 'c, 'd) Analyses.man -> ThreadIdDomain.Thread.t -> TIDs.t

reflexive-transitive closure of child relation applied to tid and filtered to only include threads, where tid is a must-ancestor

  • parameter man

    any man

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

compute all descendant threads that may run along with the ego thread at a program point. for all of them, tid must be an ancestor

  • parameter man

    man of ego thread at the program point

  • parameter tid

    ego thread id

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