> > > swfxprinter.java is in the donation and converts ABC code to text. > Something like it could be used to do analysis. > > I believe Martin meant something like a tool that mechanically proves that the generated bytecode is not erroneous. For example, if you have a conditional branch you want to check that after conditional branch joins back the execution routine all attempts to read / write from / to registers address the same (or same kind of) values. There are of course plenty of checks. Some (like this one) the compiler must do - it's a basic sanity check, but some more complex, the compiler doesn't do (for example, it is possible to analyze whether you are trying to read from a register containing null pointer) etc. These checks are usually very expensive in terms of performance, but I don't see why / how SWF execution must be involved, it's actually better if it's not involved, because some problems aren't possible to solve by a increasing the number of tests - they will tend to be infinite or just too many.
Best. Oleg