The Java Bytecode Verifier with Structured Locking Checks
			    Version 0.9

		by Gaetano Bigliardi and Cosimo Laneve

PROVISOS.

  1. The verifier works with Java 2 SDK 1.2 and later versions. 
 
  2. The verifier requires the BCEL library (bcel.sourceforge.net) to be
     already installed.

HOW TO INSTALL THE VERIFIER.

        a. In the directory where you have downloaded the file, run
        	> tar xvfzp verifyclass.tgz
	   this creates a directory "verifyclass"

        c. set the environment variable CLASSPATH in order to contain
	   the path where the verifyclass directory has been created

        d. include in the CLASSPATH variable the directory where the
           BCEL library has been installed

        e. to verify that everything is gone well, try
		> java verifyclass 
	   The verifier should print all the instructions it recognizes.

	f. You may also want to recompile the verifier. In this case,
	   run
		> make
	   in the directory "verifyclass". Additionally, to (re)generate 
	   the API documentation, it sufficies to run
		> make javadoc

USER MANUAL.

        a. To verify a class A, create a new directory and move 
           inside this new directory. Check that the path of the class 
	   A is contained into CLASSPATH (a simple way is to move 
	   A in the current directory and include "." in CLASSPATH)

        b. run
		> java verifyclass A

        c. the verifier creates a html-file for every method of the class A,
	   which is not native or abstract. These files contain the bytecode 
	   of the method and the type informations for every instruction

        d. the verification is successful, if the end of the html-file
	   contains a message
           	"Result = true"
	   Otherwise, there is a message
           	"VerifyException: ..." 
	   which specifies the erroneous instruction and the error.

THE INSTRUCTIONS WHICH ARE CHECKED.

   We insert new instructions every now and then. So, please, check the 
   current instructions with the statement
		> java verifyclass

WELL KNOWN PROBLEMS IN THE 0.9 VERSION. 

   In the version 0.9 we will not consider the instructions for subroutines
   and arrays management (jsr, ret, newarray, arraylength, aaload, aastore).

   Types char and byte are modelled in terms of integers. This may be source
   of problems.

   Most of the rules manage the type long. For some of them this type may
   be problematic (because it takes the double of the space), in particular
   the StoreRule.

Have fun!

	Gaetano and Cosimo