@@ -231,7 +231,7 @@ pragma[inline]
231
231
ControlFlowNode getAThreadContextAwarePredecessor ( ControlFlowNode start , ControlFlowNode end ) {
232
232
result = getAThreadContextAwareSuccessor ( start ) and
233
233
not result = getAThreadContextAwareSuccessor ( end ) and
234
- not result = end
234
+ not result = end
235
235
}
236
236
237
237
/**
@@ -399,16 +399,15 @@ class LockProtectedControlFlowNode extends ThreadedCFN {
399
399
not exists ( ControlFlowNode unlock |
400
400
// it's an unlock
401
401
unlock = getAThreadContextAwarePredecessor ( lock , this ) and
402
- unlock .( MutexFunctionCall ) .isUnlock ( )
402
+ unlock .( MutexFunctionCall ) .isUnlock ( ) and
403
403
// note that we don't check that it's the same lock -- this is left
404
404
// to the caller to enforce this condition.
405
-
406
405
// Because of the way that `getAThreadContextAwarePredecessor` works, it is possible
407
- // for operations PAST it to be technically part of the predecessors.
408
- // Thus, we need to make sure that this lock (to be actually)
409
- // an unlock along the same path it must be the case that when we
410
- // supply it as the starting point of the search it hits the try lock
411
- and getAThreadContextAwareSuccessor ( unlock ) = this
406
+ // for operations PAST it to be technically part of the predecessors.
407
+ // Thus, we need to make sure that this lock (to be actually)
408
+ // an unlock along the same path it must be the case that when we
409
+ // supply it as the starting point of the search it hits the try lock
410
+ getAThreadContextAwareSuccessor ( unlock ) = this
412
411
) and
413
412
( lock instanceof MutexFunctionCall implies not this .( MutexFunctionCall ) .isUnlock ( ) )
414
413
)
0 commit comments