Member predicate Handler::mayBeGloballyImpure
Holds if it is possible that this statement is globally impure.
Similar to mayBeImpure()
, except that mayBeGloballyImpure()
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()