Spec.Argmodule D = DeadlockDomain.MayLockEventsmodule V : sig ... endmodule G : sig ... endval side_lock_event_pair :
('a, G.t, 'b, Goblint_lib.LockDomain.Addr.t) Analyses.ctx ->
(Goblint_lib.LockDomain.Addr.t * Node.t * MCPAccess.A.t) ->
(G.key * Node.t * MCPAccess.A.t) ->
unitval part_access : ('a, 'b, 'c, 'd) Analyses.ctx -> MCPAccess.A.tval add :
(D.t, G.t, 'a, Goblint_lib.LockDomain.Addr.t) Analyses.ctx ->
LockDomain.Lockset.Lock.t ->
D.tval remove :
(D.t, 'a, 'b, 'c) Analyses.ctx ->
Goblint_lib.DeadlockDomain.Lock.t ->
D.t