Module MutexAnalysis.Spec
include sig ... end
val vdecl : ('a, 'b, 'c, 'd) Goblint_lib__Analyses.ctx -> 'e -> 'aval asm : ('a, 'b, 'c, 'd) Goblint_lib__Analyses.ctx -> 'aval skip : ('a, 'b, 'c, 'd) Goblint_lib__Analyses.ctx -> 'aval morphstate : 'a -> 'b -> 'bval sync : ('a, 'b, 'c, 'd) Goblint_lib__Analyses.ctx -> 'e -> 'aval context : 'a -> 'b -> 'bval assign :
('a, 'b, 'c, 'd) Goblint_lib__Analyses.ctx ->
GoblintCil.lval ->
GoblintCil.exp ->
'aval branch :
('a, 'b, 'c, 'd) Goblint_lib__Analyses.ctx ->
GoblintCil.exp ->
bool ->
'aval body :
('a, 'b, 'c, 'd) Goblint_lib__Analyses.ctx ->
GoblintCil.fundec ->
'aval return :
('a, 'b, 'c, 'd) Goblint_lib__Analyses.ctx ->
GoblintCil.exp option ->
GoblintCil.fundec ->
'aval enter :
('a, 'b, 'c, 'd) Goblint_lib__Analyses.ctx ->
GoblintCil.lval option ->
GoblintCil.fundec ->
GoblintCil.exp list ->
('a * 'a) listval combine :
'a ->
GoblintCil.lval option ->
'b ->
GoblintCil.fundec ->
GoblintCil.exp list ->
'c ->
'd ->
'dval special :
('a, 'b, 'c, 'd) Goblint_lib__Analyses.ctx ->
GoblintCil.lval option ->
GoblintCil.varinfo ->
GoblintCil.exp list ->
'aval threadspawn :
('a, 'b, 'c, 'd) Goblint_lib__Analyses.ctx ->
'e ->
'f ->
'g ->
'h ->
'aval threadenter : 'a -> 'b -> 'c -> 'd -> Arg.D.t listval name : unit -> stringval should_join : D.t -> D.t -> boolval finalize : unit -> unit