The AVM verifier when encounters and error, writes to flash log. In the documentation it says that verifier will visit "all possible branches" where jumps might take it. However it is still pretty confusing when trying to follow the output. Are there any ideas how to interpret it properly? The whole flow seems confusing.
For example what are the meanings of the following markings.
MERGE FIRST
MERGE CURRENT
MERGE TARGET
AFTER MERGE
Further, there are machine instructions and Machine State with registers, scope stack and operand stack. I understand when I see instruction and later a state modified, e.g. PushFalse would make a Boolean appear on Operand Stack - (Boolean[B]). But sometimes state is written even without an instruction preceding it, in combination with MERGE FIRST, MERGE CURRENT, etc. What does that mean?
Unfortunately this is the most comprehensive explanation I could find out there.
http://hg.mozilla.org/tamarin-redux/file/3c8d01c7b51a/doc/verifier.txt