I am currently reading the extended Version of the Paper Online Detection of Effectively Callback Free Objects with Applications of Smart Contract.
I am trying to understand the proofs of Chapter 6. In particular, I cannot understand the premise of proofs 6.2. Indeed, the authors use a variant of SMAC, an Object-oriented and Turing Complete (SMAC) and they claim that (I underlined the suspicious claim with bold)
Thus, we focus on verifying $sECF$, namely, statically verifying whether all executions of an object are $dECF_{FS}$ or $ECF_{C}$, where the domains of the object variables are restricted to finite sets. Hence, such objects can be modeled with a pushdown-automaton (PDA). Such a PDA for an object o is able to simulate any modular well-formed execution $\kappa \in \pi$ where the active object of all states in $\pi$ is o.
In my understanding, this premise should be wrong, because although the state of this SMAC program is final, it is not computable by Push-Down-Automata (which compute total functions).
Foo:
int x = 0 // field of the object
enter // enter the single method of the object/contract
while true do
x = 1
return