ECMA for CLR claims that "It shall be possible, with a single forward-pass through the CIL instruction stream for any method, to infer the exact state of the evaluation stack at every instruction"

In other words, itshall be possible to perform bytecode verification in a single forward-pass.

To make that possible , ECMA requires that

"if that single-pass analysis arrives at an

instruction, call it location X,
that immediately follows an unconditional

branch, and where X is not the
target of an earlier branch instruction, then

the state of the evaluation
stack at X shall be empty."

On the other

hand, ECMA claims that it "simulates all control flow paths".

I don't get

how this simulation of all paths is done in a "single

forward-pass".

Suppose that I have a backward branch instruction Y,

targeting an (earlier)
instruction Z. The stack state at Y has to be

"merged" with the stack state existing at Z, right?

But then, I have

to propagate again the (new) stack state at Z to its
successors. But here,

it is a contradiction with the "single forward-pass"
bytecode

verification.

My guess is the following:

• that "shall be possible" doesn't mean that the bytecode verification is performed in a single forward pass on the original bytecode stream. The code array has first to be rearranged in order to make possible the verification in a single pass. That probably happens during a JIT compilation.

• If it's not rearranged, the bytecode verification is similar to the one of JVM, i.e., a dataflow analysis with a fix point interation.
  

Please someone correct me if I'm wrong.

Thanks!