Predicate TOCTOURace::commonSynchronization

Holds if e1 and e2 appear within a synchronized block on monitor.

predicate commonSynchronization(Expr e1, Expr e2, Variable monitor)