Holds if it is possible that this statement is globally impure.
mayBeImpure(), except that
does not consider modifications to temporary local variables to be
impure. That is, if you call a function in which
mayBeGloballyImpure() doesn’t hold for any statement, then the
function as a whole will have no side-effects, even if it mutates
its own fresh stack variables.
predicate mayBeGloballyImpure ( )