I'm not familiar with Ethereum programs, but it seems to me that it's not possible to answer the practically-identical question, "How much gas does this program need to start with to guarantee it will either get into a loop or halt of its own accord before it runs out of gas?"

Or, to put it another way, it sounds like the language is Turing complete in roughly the same way C is Turing complete even though every C program ever instantiated is actually a linear bounded automaton because there's no such thing as an infinite tape.

Like, I can announce that my C-like language will always halt after a trillion-trillion operations and therefore the halting problem is "solved" for it, but for all other purposes it's almost exactly as difficult to reason about as a Turing machine.