Predicate definitionBarrier

Holds if barrier is either a (potential) definition of v or follows an access that gets the address of v. In both cases, the value of v after barrier cannot be assumed to be the same as before.