Member predicate SwitchCase :: mayBeGloballyImpure
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 ( )