Predicate TOCTOURace::alwaysLocked

Holds if all accesses to v (outside of initializers) are locked in the same way.

predicate alwaysLocked(Field f)