commons-commits mailing list archives

Site index · List index
Message view « Date » · « Thread »
Top « Date » · « Thread »
From s...@apache.org
Subject svn commit: r1598766 [9/12] - in /commons/proper/bcel/trunk/src: main/java/org/apache/bcel/ main/java/org/apache/bcel/classfile/ main/java/org/apache/bcel/generic/ main/java/org/apache/bcel/util/ main/java/org/apache/bcel/verifier/exc/ main/java/org/ap...
Date Fri, 30 May 2014 22:51:30 GMT
Modified: commons/proper/bcel/trunk/src/main/java/org/apache/bcel/verifier/structurals/InstConstraintVisitor.java
URL: http://svn.apache.org/viewvc/commons/proper/bcel/trunk/src/main/java/org/apache/bcel/verifier/structurals/InstConstraintVisitor.java?rev=1598766&r1=1598765&r2=1598766&view=diff
==============================================================================
--- commons/proper/bcel/trunk/src/main/java/org/apache/bcel/verifier/structurals/InstConstraintVisitor.java (original)
+++ commons/proper/bcel/trunk/src/main/java/org/apache/bcel/verifier/structurals/InstConstraintVisitor.java Fri May 30 22:51:27 2014
@@ -53,1206 +53,1206 @@ import org.apache.bcel.verifier.exc.Stru
  */
 public class InstConstraintVisitor extends EmptyVisitor{
 
-	private static final ObjectType GENERIC_ARRAY = ObjectType.getInstance("org.apache.bcel.verifier.structurals.GenericArray");
+    private static final ObjectType GENERIC_ARRAY = ObjectType.getInstance("org.apache.bcel.verifier.structurals.GenericArray");
 
-	/**
-	 * The constructor. Constructs a new instance of this class.
-	 */
-	public InstConstraintVisitor(){}
-
-	/**
-	 * The Execution Frame we're working on.
-	 *
-	 * @see #setFrame(Frame f)
-	 * @see #locals()
-	 * @see #stack()
-	 */
-	private Frame frame = null;
-
-	/**
-	 * The ConstantPoolGen we're working on.
-	 * 
-	 * @see #setConstantPoolGen(ConstantPoolGen cpg)
-	 */
-	private ConstantPoolGen cpg = null;
-
-	/**
-	 * The MethodGen we're working on.
-	 * 
-	 * @see #setMethodGen(MethodGen mg)
-	 */
-	private MethodGen mg = null;
-
-	/**
-	 * The OperandStack we're working on.
-	 *
-	 * @see #setFrame(Frame f)
-	 */
-	private OperandStack stack(){
-		return frame.getStack();
-	}
-
-	/**
-	 * The LocalVariables we're working on.
-	 *
-	 * @see #setFrame(Frame f)
-	 */
-	private LocalVariables locals(){
-		return frame.getLocals();
-	}
+    /**
+     * The constructor. Constructs a new instance of this class.
+     */
+    public InstConstraintVisitor(){}
+
+    /**
+     * The Execution Frame we're working on.
+     *
+     * @see #setFrame(Frame f)
+     * @see #locals()
+     * @see #stack()
+     */
+    private Frame frame = null;
+
+    /**
+     * The ConstantPoolGen we're working on.
+     * 
+     * @see #setConstantPoolGen(ConstantPoolGen cpg)
+     */
+    private ConstantPoolGen cpg = null;
+
+    /**
+     * The MethodGen we're working on.
+     * 
+     * @see #setMethodGen(MethodGen mg)
+     */
+    private MethodGen mg = null;
+
+    /**
+     * The OperandStack we're working on.
+     *
+     * @see #setFrame(Frame f)
+     */
+    private OperandStack stack(){
+        return frame.getStack();
+    }
+
+    /**
+     * The LocalVariables we're working on.
+     *
+     * @see #setFrame(Frame f)
+     */
+    private LocalVariables locals(){
+        return frame.getLocals();
+    }
 
-	/**
+    /**
    * This method is called by the visitXXX() to notify the acceptor of this InstConstraintVisitor
    * that a constraint violation has occured. This is done by throwing an instance of a
    * StructuralCodeConstraintException.
    * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException always.
    */
-	private void constraintViolated(Instruction violator, String description){
-		String fq_classname = violator.getClass().getName();
-		throw new StructuralCodeConstraintException("Instruction "+ fq_classname.substring(fq_classname.lastIndexOf('.')+1) +" constraint violated: " + description);
-	}
-
-	/**
-	 * This returns the single instance of the InstConstraintVisitor class.
-	 * To operate correctly, other values must have been set before actually
-	 * using the instance.
-	 * Use this method for performance reasons.
-	 *
-	 * @see #setConstantPoolGen(ConstantPoolGen cpg)
-	 * @see #setMethodGen(MethodGen mg)
-	 */
-	public void setFrame(Frame f){
-		this.frame = f;
-		//if (singleInstance.mg == null || singleInstance.cpg == null) throw new AssertionViolatedException("Forgot to set important values first.");
-	}
-
-	/**
-	 * Sets the ConstantPoolGen instance needed for constraint
-	 * checking prior to execution.
-	 */	
-	public void setConstantPoolGen(ConstantPoolGen cpg){
-		this.cpg = cpg;
-	}
-
-	/**
-	 * Sets the MethodGen instance needed for constraint
-	 * checking prior to execution.
-	 */
-	public void setMethodGen(MethodGen mg){
-		this.mg = mg;
-	}
-
-	/**
-	 * Assures index is of type INT.
-	 * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied.
-	 */
-	private void indexOfInt(Instruction o, Type index){
-		if (! index.equals(Type.INT)) {
+    private void constraintViolated(Instruction violator, String description){
+        String fq_classname = violator.getClass().getName();
+        throw new StructuralCodeConstraintException("Instruction "+ fq_classname.substring(fq_classname.lastIndexOf('.')+1) +" constraint violated: " + description);
+    }
+
+    /**
+     * This returns the single instance of the InstConstraintVisitor class.
+     * To operate correctly, other values must have been set before actually
+     * using the instance.
+     * Use this method for performance reasons.
+     *
+     * @see #setConstantPoolGen(ConstantPoolGen cpg)
+     * @see #setMethodGen(MethodGen mg)
+     */
+    public void setFrame(Frame f){
+        this.frame = f;
+        //if (singleInstance.mg == null || singleInstance.cpg == null) throw new AssertionViolatedException("Forgot to set important values first.");
+    }
+
+    /**
+     * Sets the ConstantPoolGen instance needed for constraint
+     * checking prior to execution.
+     */    
+    public void setConstantPoolGen(ConstantPoolGen cpg){
+        this.cpg = cpg;
+    }
+
+    /**
+     * Sets the MethodGen instance needed for constraint
+     * checking prior to execution.
+     */
+    public void setMethodGen(MethodGen mg){
+        this.mg = mg;
+    }
+
+    /**
+     * Assures index is of type INT.
+     * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied.
+     */
+    private void indexOfInt(Instruction o, Type index){
+        if (! index.equals(Type.INT)) {
             constraintViolated(o, "The 'index' is not of type int but of type "+index+".");
         }
-	}
+    }
 
-	/**
-	 * Assures the ReferenceType r is initialized (or Type.NULL).
-	 * Formally, this means (!(r instanceof UninitializedObjectType)), because
-	 * there are no uninitialized array types.
-	 * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied.
-	 */
-	private void referenceTypeIsInitialized(Instruction o, ReferenceType r){
-		if (r instanceof UninitializedObjectType){
-			constraintViolated(o, "Working on an uninitialized object '"+r+"'.");
-		}
-	}
-
-	/** Assures value is of type INT. */
-	private void valueOfInt(Instruction o, Type value){
-		if (! value.equals(Type.INT)) {
+    /**
+     * Assures the ReferenceType r is initialized (or Type.NULL).
+     * Formally, this means (!(r instanceof UninitializedObjectType)), because
+     * there are no uninitialized array types.
+     * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied.
+     */
+    private void referenceTypeIsInitialized(Instruction o, ReferenceType r){
+        if (r instanceof UninitializedObjectType){
+            constraintViolated(o, "Working on an uninitialized object '"+r+"'.");
+        }
+    }
+
+    /** Assures value is of type INT. */
+    private void valueOfInt(Instruction o, Type value){
+        if (! value.equals(Type.INT)) {
             constraintViolated(o, "The 'value' is not of type int but of type "+value+".");
         }
-	}
+    }
 
-	/**
-	 * Assures arrayref is of ArrayType or NULL;
-	 * returns true if and only if arrayref is non-NULL.
-	 * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is violated.
- 	 */
-	private boolean arrayrefOfArrayType(Instruction o, Type arrayref){
-		if (! ((arrayref instanceof ArrayType) || arrayref.equals(Type.NULL)) ) {
+    /**
+     * Assures arrayref is of ArrayType or NULL;
+     * returns true if and only if arrayref is non-NULL.
+     * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is violated.
+      */
+    private boolean arrayrefOfArrayType(Instruction o, Type arrayref){
+        if (! ((arrayref instanceof ArrayType) || arrayref.equals(Type.NULL)) ) {
             constraintViolated(o, "The 'arrayref' does not refer to an array but is of type "+arrayref+".");
         }
-		return (arrayref instanceof ArrayType);
-	}
+        return (arrayref instanceof ArrayType);
+    }
+
+    /***************************************************************/
+    /* MISC                                                        */
+    /***************************************************************/
+    /**
+     * Ensures the general preconditions of an instruction that accesses the stack.
+     * This method is here because BCEL has no such superinterface for the stack
+     * accessing instructions; and there are funny unexpected exceptions in the
+     * semantices of the superinterfaces and superclasses provided.
+     * E.g. SWAP is a StackConsumer, but DUP_X1 is not a StackProducer.
+     * Therefore, this method is called by all StackProducer, StackConsumer,
+     * and StackInstruction instances via their visitXXX() method.
+     * Unfortunately, as the superclasses and superinterfaces overlap, some instructions
+     * cause this method to be called two or three times. [TODO: Fix this.]
+     *
+     * @see #visitStackConsumer(StackConsumer o)
+     * @see #visitStackProducer(StackProducer o)
+     * @see #visitStackInstruction(StackInstruction o)
+     */
+    private void _visitStackAccessor(Instruction o){
+        int consume = o.consumeStack(cpg); // Stack values are always consumed first; then produced.
+        if (consume > stack().slotsUsed()){
+            constraintViolated(o, "Cannot consume "+consume+" stack slots: only "+stack().slotsUsed()+" slot(s) left on stack!\nStack:\n"+stack());
+        }
 
-	/***************************************************************/
-	/* MISC                                                        */
-	/***************************************************************/
-	/**
-	 * Ensures the general preconditions of an instruction that accesses the stack.
-	 * This method is here because BCEL has no such superinterface for the stack
-	 * accessing instructions; and there are funny unexpected exceptions in the
-	 * semantices of the superinterfaces and superclasses provided.
-	 * E.g. SWAP is a StackConsumer, but DUP_X1 is not a StackProducer.
-	 * Therefore, this method is called by all StackProducer, StackConsumer,
-	 * and StackInstruction instances via their visitXXX() method.
-	 * Unfortunately, as the superclasses and superinterfaces overlap, some instructions
-	 * cause this method to be called two or three times. [TODO: Fix this.]
-	 *
-	 * @see #visitStackConsumer(StackConsumer o)
-	 * @see #visitStackProducer(StackProducer o)
-	 * @see #visitStackInstruction(StackInstruction o)
-	 */
-	private void _visitStackAccessor(Instruction o){
-		int consume = o.consumeStack(cpg); // Stack values are always consumed first; then produced.
-		if (consume > stack().slotsUsed()){
-			constraintViolated(o, "Cannot consume "+consume+" stack slots: only "+stack().slotsUsed()+" slot(s) left on stack!\nStack:\n"+stack());
-		}
-
-		int produce = o.produceStack(cpg) - o.consumeStack(cpg); // Stack values are always consumed first; then produced.
-		if ( produce + stack().slotsUsed() > stack().maxStack() ){
-			constraintViolated(o, "Cannot produce "+produce+" stack slots: only "+(stack().maxStack()-stack().slotsUsed())+" free stack slot(s) left.\nStack:\n"+stack());
-		}
-	}
-
-	/***************************************************************/
-	/* "generic"visitXXXX methods where XXXX is an interface       */
-	/* therefore, we don't know the order of visiting; but we know */
-	/* these methods are called before the visitYYYY methods below */
-	/***************************************************************/
-
-	/**
-	 * Assures the generic preconditions of a LoadClass instance.
-	 * The referenced class is loaded and pass2-verified.
-	 */
-	@Override
+        int produce = o.produceStack(cpg) - o.consumeStack(cpg); // Stack values are always consumed first; then produced.
+        if ( produce + stack().slotsUsed() > stack().maxStack() ){
+            constraintViolated(o, "Cannot produce "+produce+" stack slots: only "+(stack().maxStack()-stack().slotsUsed())+" free stack slot(s) left.\nStack:\n"+stack());
+        }
+    }
+
+    /***************************************************************/
+    /* "generic"visitXXXX methods where XXXX is an interface       */
+    /* therefore, we don't know the order of visiting; but we know */
+    /* these methods are called before the visitYYYY methods below */
+    /***************************************************************/
+
+    /**
+     * Assures the generic preconditions of a LoadClass instance.
+     * The referenced class is loaded and pass2-verified.
+     */
+    @Override
     public void visitLoadClass(LoadClass o){
-		ObjectType t = o.getLoadClassType(cpg);
-		if (t != null){// null means "no class is loaded"
-			Verifier v = VerifierFactory.getVerifier(t.getClassName());
-			VerificationResult vr = v.doPass2();
-			if (vr.getStatus() != VerificationResult.VERIFIED_OK){
-				constraintViolated((Instruction) o, "Class '"+o.getLoadClassType(cpg).getClassName()+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
-			}
-		}
-	}
-
-	/**
-	 * Ensures the general preconditions of a StackConsumer instance.
-	 */
-	@Override
+        ObjectType t = o.getLoadClassType(cpg);
+        if (t != null){// null means "no class is loaded"
+            Verifier v = VerifierFactory.getVerifier(t.getClassName());
+            VerificationResult vr = v.doPass2();
+            if (vr.getStatus() != VerificationResult.VERIFIED_OK){
+                constraintViolated((Instruction) o, "Class '"+o.getLoadClassType(cpg).getClassName()+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
+            }
+        }
+    }
+
+    /**
+     * Ensures the general preconditions of a StackConsumer instance.
+     */
+    @Override
     public void visitStackConsumer(StackConsumer o){
-		_visitStackAccessor((Instruction) o);
-	}
-	
-	/**
-	 * Ensures the general preconditions of a StackProducer instance.
-	 */
-	@Override
+        _visitStackAccessor((Instruction) o);
+    }
+
+    /**
+     * Ensures the general preconditions of a StackProducer instance.
+     */
+    @Override
     public void visitStackProducer(StackProducer o){
-		_visitStackAccessor((Instruction) o);
-	}
+        _visitStackAccessor((Instruction) o);
+    }
 
 
-	/***************************************************************/
-	/* "generic" visitYYYY methods where YYYY is a superclass.     */
-	/* therefore, we know the order of visiting; we know           */
-	/* these methods are called after the visitXXXX methods above. */
-	/***************************************************************/
-	/**
-	 * Ensures the general preconditions of a CPInstruction instance.
-	 */
-	@Override
+    /***************************************************************/
+    /* "generic" visitYYYY methods where YYYY is a superclass.     */
+    /* therefore, we know the order of visiting; we know           */
+    /* these methods are called after the visitXXXX methods above. */
+    /***************************************************************/
+    /**
+     * Ensures the general preconditions of a CPInstruction instance.
+     */
+    @Override
     public void visitCPInstruction(CPInstruction o){
-		int idx = o.getIndex();
-		if ((idx < 0) || (idx >= cpg.getSize())){
-			throw new AssertionViolatedException("Huh?! Constant pool index of instruction '"+o+"' illegal? Pass 3a should have checked this!");
-		}
-	}
-
-	/**
-	 * Ensures the general preconditions of a FieldInstruction instance.
-	 */
-	 @Override
+        int idx = o.getIndex();
+        if ((idx < 0) || (idx >= cpg.getSize())){
+            throw new AssertionViolatedException("Huh?! Constant pool index of instruction '"+o+"' illegal? Pass 3a should have checked this!");
+        }
+    }
+
+    /**
+     * Ensures the general preconditions of a FieldInstruction instance.
+     */
+     @Override
     public void visitFieldInstruction(FieldInstruction o){
-	 	// visitLoadClass(o) has been called before: Every FieldOrMethod
-	 	// implements LoadClass.
-	 	// visitCPInstruction(o) has been called before.
-		// A FieldInstruction may be: GETFIELD, GETSTATIC, PUTFIELD, PUTSTATIC 
-			Constant c = cpg.getConstant(o.getIndex());
-			if (!(c instanceof ConstantFieldref)){
-				constraintViolated(o, "Index '"+o.getIndex()+"' should refer to a CONSTANT_Fieldref_info structure, but refers to '"+c+"'.");
-			}
-			// the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
-			Type t = o.getType(cpg);
-			if (t instanceof ObjectType){
-				String name = ((ObjectType)t).getClassName();
-				Verifier v = VerifierFactory.getVerifier( name );
-				VerificationResult vr = v.doPass2();
-				if (vr.getStatus() != VerificationResult.VERIFIED_OK){
-					constraintViolated(o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
-				}
-			}
-	 }
-	 
-	/**
-	 * Ensures the general preconditions of an InvokeInstruction instance.
-	 */
-	 @Override
+         // visitLoadClass(o) has been called before: Every FieldOrMethod
+         // implements LoadClass.
+         // visitCPInstruction(o) has been called before.
+        // A FieldInstruction may be: GETFIELD, GETSTATIC, PUTFIELD, PUTSTATIC 
+            Constant c = cpg.getConstant(o.getIndex());
+            if (!(c instanceof ConstantFieldref)){
+                constraintViolated(o, "Index '"+o.getIndex()+"' should refer to a CONSTANT_Fieldref_info structure, but refers to '"+c+"'.");
+            }
+            // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
+            Type t = o.getType(cpg);
+            if (t instanceof ObjectType){
+                String name = ((ObjectType)t).getClassName();
+                Verifier v = VerifierFactory.getVerifier( name );
+                VerificationResult vr = v.doPass2();
+                if (vr.getStatus() != VerificationResult.VERIFIED_OK){
+                    constraintViolated(o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
+                }
+            }
+     }
+
+    /**
+     * Ensures the general preconditions of an InvokeInstruction instance.
+     */
+     @Override
     public void visitInvokeInstruction(InvokeInstruction o){
-	 	// visitLoadClass(o) has been called before: Every FieldOrMethod
-	 	// implements LoadClass.
-	 	// visitCPInstruction(o) has been called before.
+         // visitLoadClass(o) has been called before: Every FieldOrMethod
+         // implements LoadClass.
+         // visitCPInstruction(o) has been called before.
         //TODO
-	 }
-	 
-	/**
-	 * Ensures the general preconditions of a StackInstruction instance.
-	 */
-	@Override
+     }
+
+    /**
+     * Ensures the general preconditions of a StackInstruction instance.
+     */
+    @Override
     public void visitStackInstruction(StackInstruction o){
-		_visitStackAccessor(o);
-	}
+        _visitStackAccessor(o);
+    }
 
-	/**
-	 * Assures the generic preconditions of a LocalVariableInstruction instance.
-	 * That is, the index of the local variable must be valid.
-	 */
-	@Override
+    /**
+     * Assures the generic preconditions of a LocalVariableInstruction instance.
+     * That is, the index of the local variable must be valid.
+     */
+    @Override
     public void visitLocalVariableInstruction(LocalVariableInstruction o){
-		if (locals().maxLocals() <= (o.getType(cpg).getSize()==1? o.getIndex() : o.getIndex()+1) ){
-			constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
-		}
-	}
-	
-	/**
-	 * Assures the generic preconditions of a LoadInstruction instance.
-	 */
-	@Override
+        if (locals().maxLocals() <= (o.getType(cpg).getSize()==1? o.getIndex() : o.getIndex()+1) ){
+            constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
+        }
+    }
+
+    /**
+     * Assures the generic preconditions of a LoadInstruction instance.
+     */
+    @Override
     public void visitLoadInstruction(LoadInstruction o){
-		//visitLocalVariableInstruction(o) is called before, because it is more generic.
+        //visitLocalVariableInstruction(o) is called before, because it is more generic.
+
+        // LOAD instructions must not read Type.UNKNOWN
+        if (locals().get(o.getIndex()) == Type.UNKNOWN){
+            constraintViolated(o, "Read-Access on local variable "+o.getIndex()+" with unknown content.");
+        }
+
+        // LOAD instructions, two-slot-values at index N must have Type.UNKNOWN
+        // as a symbol for the higher halve at index N+1
+        // [suppose some instruction put an int at N+1--- our double at N is defective]
+        if (o.getType(cpg).getSize() == 2){
+            if (locals().get(o.getIndex()+1) != Type.UNKNOWN){
+                constraintViolated(o, "Reading a two-locals value from local variables "+o.getIndex()+" and "+(o.getIndex()+1)+" where the latter one is destroyed.");
+            }
+        }
 
-		// LOAD instructions must not read Type.UNKNOWN
-		if (locals().get(o.getIndex()) == Type.UNKNOWN){
-			constraintViolated(o, "Read-Access on local variable "+o.getIndex()+" with unknown content.");
-		}
-
-		// LOAD instructions, two-slot-values at index N must have Type.UNKNOWN
-		// as a symbol for the higher halve at index N+1
-		// [suppose some instruction put an int at N+1--- our double at N is defective]
-		if (o.getType(cpg).getSize() == 2){
-			if (locals().get(o.getIndex()+1) != Type.UNKNOWN){
-				constraintViolated(o, "Reading a two-locals value from local variables "+o.getIndex()+" and "+(o.getIndex()+1)+" where the latter one is destroyed.");
-			}
-		}
-
-		// LOAD instructions must read the correct type.
-		if (!(o instanceof ALOAD)){
-			if (locals().get(o.getIndex()) != o.getType(cpg) ){
-				constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction type: '"+o.getType(cpg)+"'.");
-			}
-		}
-		else{ // we deal with an ALOAD
-			if (!(locals().get(o.getIndex()) instanceof ReferenceType)){
-				constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction expects a ReferenceType.");
-			}
-			// ALOAD __IS ALLOWED__ to put uninitialized objects onto the stack!
-			//referenceTypeIsInitialized(o, (ReferenceType) (locals().get(o.getIndex())));
-		}
-
-		// LOAD instructions must have enough free stack slots.
-		if ((stack().maxStack() - stack().slotsUsed()) < o.getType(cpg).getSize()){
-			constraintViolated(o, "Not enough free stack slots to load a '"+o.getType(cpg)+"' onto the OperandStack.");
-		}
-	}
-
-	/**
-	 * Assures the generic preconditions of a StoreInstruction instance.
-	 */
-	@Override
+        // LOAD instructions must read the correct type.
+        if (!(o instanceof ALOAD)){
+            if (locals().get(o.getIndex()) != o.getType(cpg) ){
+                constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction type: '"+o.getType(cpg)+"'.");
+            }
+        }
+        else{ // we deal with an ALOAD
+            if (!(locals().get(o.getIndex()) instanceof ReferenceType)){
+                constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction expects a ReferenceType.");
+            }
+            // ALOAD __IS ALLOWED__ to put uninitialized objects onto the stack!
+            //referenceTypeIsInitialized(o, (ReferenceType) (locals().get(o.getIndex())));
+        }
+
+        // LOAD instructions must have enough free stack slots.
+        if ((stack().maxStack() - stack().slotsUsed()) < o.getType(cpg).getSize()){
+            constraintViolated(o, "Not enough free stack slots to load a '"+o.getType(cpg)+"' onto the OperandStack.");
+        }
+    }
+
+    /**
+     * Assures the generic preconditions of a StoreInstruction instance.
+     */
+    @Override
     public void visitStoreInstruction(StoreInstruction o){
-		//visitLocalVariableInstruction(o) is called before, because it is more generic.
+        //visitLocalVariableInstruction(o) is called before, because it is more generic.
+
+        if (stack().isEmpty()){ // Don't bother about 1 or 2 stack slots used. This check is implicitely done below while type checking.
+            constraintViolated(o, "Cannot STORE: Stack to read from is empty.");
+        }
+
+        if ( (!(o instanceof ASTORE)) ){
+            if (! (stack().peek() == o.getType(cpg)) ){// the other xSTORE types are singletons in BCEL.
+                constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction type: '"+o.getType(cpg)+"'.");
+            }
+        }
+        else{ // we deal with ASTORE
+            Type stacktop = stack().peek();
+            if ( (!(stacktop instanceof ReferenceType)) && (!(stacktop instanceof ReturnaddressType)) ){
+                constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction expects a ReferenceType or a ReturnadressType.");
+            }
+            //if (stacktop instanceof ReferenceType){
+            //    referenceTypeIsInitialized(o, (ReferenceType) stacktop);
+            //}
+        }
+    }
 
-		if (stack().isEmpty()){ // Don't bother about 1 or 2 stack slots used. This check is implicitely done below while type checking.
-			constraintViolated(o, "Cannot STORE: Stack to read from is empty.");
-		}
-
-		if ( (!(o instanceof ASTORE)) ){
-			if (! (stack().peek() == o.getType(cpg)) ){// the other xSTORE types are singletons in BCEL.
-				constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction type: '"+o.getType(cpg)+"'.");
-			}
-		}
-		else{ // we deal with ASTORE
-			Type stacktop = stack().peek();
-			if ( (!(stacktop instanceof ReferenceType)) && (!(stacktop instanceof ReturnaddressType)) ){
-				constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction expects a ReferenceType or a ReturnadressType.");
-			}
-			//if (stacktop instanceof ReferenceType){
-			//	referenceTypeIsInitialized(o, (ReferenceType) stacktop);
-			//}
-		}
-	}
-
-	/**
-	 * Assures the generic preconditions of a ReturnInstruction instance.
-	 */
-	@Override
+    /**
+     * Assures the generic preconditions of a ReturnInstruction instance.
+     */
+    @Override
     public void visitReturnInstruction(ReturnInstruction o){
-		Type method_type = mg.getType();
-		if (method_type == Type.BOOLEAN ||
-			method_type == Type.BYTE ||
-			method_type == Type.SHORT ||
-			method_type == Type.CHAR){
-		        method_type = Type.INT;
-			}
+        Type method_type = mg.getType();
+        if (method_type == Type.BOOLEAN ||
+            method_type == Type.BYTE ||
+            method_type == Type.SHORT ||
+            method_type == Type.CHAR){
+                method_type = Type.INT;
+            }
 
         if (o instanceof RETURN){
             if (method_type != Type.VOID){
                 constraintViolated(o, "RETURN instruction in non-void method.");
             }
             else{
-			    return;
+                return;
+            }
+        }
+        if (o instanceof ARETURN){
+            if (stack().peek() == Type.NULL){
+                return;
+            }
+            else{
+                if (! (stack().peek() instanceof ReferenceType)){
+                    constraintViolated(o, "Reference type expected on top of stack, but is: '"+stack().peek()+"'.");
+                }
+                referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()));
+                //ReferenceType objectref = (ReferenceType) (stack().peek());
+                // TODO: This can only be checked if using Staerk-et-al's "set of object types" instead of a
+                // "wider cast object type" created during verification.
+                //if (! (objectref.isAssignmentCompatibleWith(mg.getType())) ){
+                //    constraintViolated(o, "Type on stack top which should be returned is a '"+stack().peek()+"' which is not assignment compatible with the return type of this method, '"+mg.getType()+"'.");
+                //}
             }
-		}
-		if (o instanceof ARETURN){
-			if (stack().peek() == Type.NULL){
-				return;
-			}
-			else{
-				if (! (stack().peek() instanceof ReferenceType)){
-					constraintViolated(o, "Reference type expected on top of stack, but is: '"+stack().peek()+"'.");
-				}
-				referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()));
-				//ReferenceType objectref = (ReferenceType) (stack().peek());
-				// TODO: This can only be checked if using Staerk-et-al's "set of object types" instead of a
-				// "wider cast object type" created during verification.
-				//if (! (objectref.isAssignmentCompatibleWith(mg.getType())) ){
-				//	constraintViolated(o, "Type on stack top which should be returned is a '"+stack().peek()+"' which is not assignment compatible with the return type of this method, '"+mg.getType()+"'.");
-				//}
-			}
-		}
-		else{
-			if (! ( method_type.equals( stack().peek() ))){
-				constraintViolated(o, "Current method has return type of '"+mg.getType()+"' expecting a '"+method_type+"' on top of the stack. But stack top is a '"+stack().peek()+"'.");
-			}
-		}
-	}
-
-	/***************************************************************/
-	/* "special"visitXXXX methods for one type of instruction each */
-	/***************************************************************/
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        }
+        else{
+            if (! ( method_type.equals( stack().peek() ))){
+                constraintViolated(o, "Current method has return type of '"+mg.getType()+"' expecting a '"+method_type+"' on top of the stack. But stack top is a '"+stack().peek()+"'.");
+            }
+        }
+    }
+
+    /***************************************************************/
+    /* "special"visitXXXX methods for one type of instruction each */
+    /***************************************************************/
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitAALOAD(AALOAD o){
-		Type arrayref = stack().peek(1);
-		Type index    = stack().peek(0);
-		
-		indexOfInt(o, index);
-		if (arrayrefOfArrayType(o, arrayref)){
-			if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){
-				constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+".");
-			}	
-			//referenceTypeIsInitialized(o, (ReferenceType) (((ArrayType) arrayref).getElementType()));
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        Type arrayref = stack().peek(1);
+        Type index    = stack().peek(0);
+
+        indexOfInt(o, index);
+        if (arrayrefOfArrayType(o, arrayref)){
+            if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){
+                constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+".");
+            }    
+            //referenceTypeIsInitialized(o, (ReferenceType) (((ArrayType) arrayref).getElementType()));
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitAASTORE(AASTORE o){
-	    try {
-		Type arrayref = stack().peek(2);
-		Type index    = stack().peek(1);
-		Type value    = stack().peek(0);
-
-		indexOfInt(o, index);
-		if (!(value instanceof ReferenceType)){
-			constraintViolated(o, "The 'value' is not of a ReferenceType but of type "+value+".");
-		}else{
-			//referenceTypeIsInitialized(o, (ReferenceType) value);
-		}
-		// Don't bother further with "referenceTypeIsInitialized()", there are no arrays
-		// of an uninitialized object type. 
-		if (arrayrefOfArrayType(o, arrayref)){
-			if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){
-				constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+".");
-			}
-			if (! ((ReferenceType)value).isAssignmentCompatibleWith(((ArrayType) arrayref).getElementType())){
-				constraintViolated(o, "The type of 'value' ('"+value+"') is not assignment compatible to the components of the array 'arrayref' refers to. ('"+((ArrayType) arrayref).getElementType()+"')");
-			}
-		}
-	    } catch (ClassNotFoundException e) {
-		// FIXME: maybe not the best way to handle this
-		throw new AssertionViolatedException("Missing class: " + e, e);
-	    }
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        try {
+        Type arrayref = stack().peek(2);
+        Type index    = stack().peek(1);
+        Type value    = stack().peek(0);
+
+        indexOfInt(o, index);
+        if (!(value instanceof ReferenceType)){
+            constraintViolated(o, "The 'value' is not of a ReferenceType but of type "+value+".");
+        }else{
+            //referenceTypeIsInitialized(o, (ReferenceType) value);
+        }
+        // Don't bother further with "referenceTypeIsInitialized()", there are no arrays
+        // of an uninitialized object type. 
+        if (arrayrefOfArrayType(o, arrayref)){
+            if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){
+                constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+".");
+            }
+            if (! ((ReferenceType)value).isAssignmentCompatibleWith(((ArrayType) arrayref).getElementType())){
+                constraintViolated(o, "The type of 'value' ('"+value+"') is not assignment compatible to the components of the array 'arrayref' refers to. ('"+((ArrayType) arrayref).getElementType()+"')");
+            }
+        }
+        } catch (ClassNotFoundException e) {
+        // FIXME: maybe not the best way to handle this
+        throw new AssertionViolatedException("Missing class: " + e, e);
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitACONST_NULL(ACONST_NULL o){
-		// Nothing needs to be done here.
-	}
+        // Nothing needs to be done here.
+    }
 
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitALOAD(ALOAD o){
-		//visitLoadInstruction(LoadInstruction) is called before.
-		
-		// Nothing else needs to be done here.
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        //visitLoadInstruction(LoadInstruction) is called before.
+
+        // Nothing else needs to be done here.
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitANEWARRAY(ANEWARRAY o){
-		if (!stack().peek().equals(Type.INT)) {
+        if (!stack().peek().equals(Type.INT)) {
             constraintViolated(o, "The 'count' at the stack top is not of type '"+Type.INT+"' but of type '"+stack().peek()+"'.");
-		// The runtime constant pool item at that index must be a symbolic reference to a class,
-		// array, or interface type. See Pass 3a.
+        // The runtime constant pool item at that index must be a symbolic reference to a class,
+        // array, or interface type. See Pass 3a.
         }
-	}
-	
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitARETURN(ARETURN o){
-		if (! (stack().peek() instanceof ReferenceType) ){
-			constraintViolated(o, "The 'objectref' at the stack top is not of a ReferenceType but of type '"+stack().peek()+"'.");
-		}
-		ReferenceType objectref = (ReferenceType) (stack().peek());
-		referenceTypeIsInitialized(o, objectref);
-		
-		// The check below should already done via visitReturnInstruction(ReturnInstruction), see there.
-		// It cannot be done using Staerk-et-al's "set of object types" instead of a
-		// "wider cast object type", anyway.
-		//if (! objectref.isAssignmentCompatibleWith(mg.getReturnType() )){
-		//	constraintViolated(o, "The 'objectref' type "+objectref+" at the stack top is not assignment compatible with the return type '"+mg.getReturnType()+"' of the method.");
-		//}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (! (stack().peek() instanceof ReferenceType) ){
+            constraintViolated(o, "The 'objectref' at the stack top is not of a ReferenceType but of type '"+stack().peek()+"'.");
+        }
+        ReferenceType objectref = (ReferenceType) (stack().peek());
+        referenceTypeIsInitialized(o, objectref);
+
+        // The check below should already done via visitReturnInstruction(ReturnInstruction), see there.
+        // It cannot be done using Staerk-et-al's "set of object types" instead of a
+        // "wider cast object type", anyway.
+        //if (! objectref.isAssignmentCompatibleWith(mg.getReturnType() )){
+        //    constraintViolated(o, "The 'objectref' type "+objectref+" at the stack top is not assignment compatible with the return type '"+mg.getReturnType()+"' of the method.");
+        //}
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitARRAYLENGTH(ARRAYLENGTH o){
-		Type arrayref = stack().peek(0);
-		arrayrefOfArrayType(o, arrayref);
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        Type arrayref = stack().peek(0);
+        arrayrefOfArrayType(o, arrayref);
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitASTORE(ASTORE o){
-		if (! ( (stack().peek() instanceof ReferenceType) || (stack().peek() instanceof ReturnaddressType) ) ){
-			constraintViolated(o, "The 'objectref' is not of a ReferenceType or of ReturnaddressType but of "+stack().peek()+".");
-		}
-		//if (stack().peek() instanceof ReferenceType){
-		//	referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
-		//}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (! ( (stack().peek() instanceof ReferenceType) || (stack().peek() instanceof ReturnaddressType) ) ){
+            constraintViolated(o, "The 'objectref' is not of a ReferenceType or of ReturnaddressType but of "+stack().peek()+".");
+        }
+        //if (stack().peek() instanceof ReferenceType){
+        //    referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
+        //}
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitATHROW(ATHROW o){
-	    try {
-		// It's stated that 'objectref' must be of a ReferenceType --- but since Throwable is
-		// not derived from an ArrayType, it follows that 'objectref' must be of an ObjectType or Type.NULL.
-		if (! ((stack().peek() instanceof ObjectType) || (stack().peek().equals(Type.NULL))) ){
-			constraintViolated(o, "The 'objectref' is not of an (initialized) ObjectType but of type "+stack().peek()+".");
-		}
-		
-		// NULL is a subclass of every class, so to speak.
-		if (stack().peek().equals(Type.NULL)) {
+        try {
+        // It's stated that 'objectref' must be of a ReferenceType --- but since Throwable is
+        // not derived from an ArrayType, it follows that 'objectref' must be of an ObjectType or Type.NULL.
+        if (! ((stack().peek() instanceof ObjectType) || (stack().peek().equals(Type.NULL))) ){
+            constraintViolated(o, "The 'objectref' is not of an (initialized) ObjectType but of type "+stack().peek()+".");
+        }
+
+        // NULL is a subclass of every class, so to speak.
+        if (stack().peek().equals(Type.NULL)) {
             return;
         }
-				
-		ObjectType exc = (ObjectType) (stack().peek());
-		ObjectType throwable = (ObjectType) (Type.getType("Ljava/lang/Throwable;"));
-		if ( (! (exc.subclassOf(throwable)) ) && (! (exc.equals(throwable))) ){
-			constraintViolated(o, "The 'objectref' is not of class Throwable or of a subclass of Throwable, but of '"+stack().peek()+"'.");
-		}
-	    } catch (ClassNotFoundException e) {
-		// FIXME: maybe not the best way to handle this
-		throw new AssertionViolatedException("Missing class: " + e, e);
-	    }
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+
+        ObjectType exc = (ObjectType) (stack().peek());
+        ObjectType throwable = (ObjectType) (Type.getType("Ljava/lang/Throwable;"));
+        if ( (! (exc.subclassOf(throwable)) ) && (! (exc.equals(throwable))) ){
+            constraintViolated(o, "The 'objectref' is not of class Throwable or of a subclass of Throwable, but of '"+stack().peek()+"'.");
+        }
+        } catch (ClassNotFoundException e) {
+        // FIXME: maybe not the best way to handle this
+        throw new AssertionViolatedException("Missing class: " + e, e);
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitBALOAD(BALOAD o){
-		Type arrayref = stack().peek(1);
-		Type index    = stack().peek(0);
-		indexOfInt(o, index);
-		if (arrayrefOfArrayType(o, arrayref)){
-			if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
-		 	       (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ){
-				constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"+((ArrayType) arrayref).getElementType()+"'.");
-			}
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        Type arrayref = stack().peek(1);
+        Type index    = stack().peek(0);
+        indexOfInt(o, index);
+        if (arrayrefOfArrayType(o, arrayref)){
+            if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
+                    (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ){
+                constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"+((ArrayType) arrayref).getElementType()+"'.");
+            }
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitBASTORE(BASTORE o){
-		Type arrayref = stack().peek(2);
-		Type index    = stack().peek(1);
-		Type value    = stack().peek(0);
-
-		indexOfInt(o, index);
-		valueOfInt(o, value);
-		if (arrayrefOfArrayType(o, arrayref)){
-			if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
-			        (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ) {
+        Type arrayref = stack().peek(2);
+        Type index    = stack().peek(1);
+        Type value    = stack().peek(0);
+
+        indexOfInt(o, index);
+        valueOfInt(o, value);
+        if (arrayrefOfArrayType(o, arrayref)){
+            if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
+                    (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ) {
                 constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"+((ArrayType) arrayref).getElementType()+"'.");
             }
-		}
-	}
+        }
+    }
 
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitBIPUSH(BIPUSH o){
-		// Nothing to do...
-	}
+        // Nothing to do...
+    }
 
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitBREAKPOINT(BREAKPOINT o){
-		throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as BREAKPOINT.");
-	}
+        throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as BREAKPOINT.");
+    }
 
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitCALOAD(CALOAD o){
-		Type arrayref = stack().peek(1);
-		Type index = stack().peek(0);
-		
-		indexOfInt(o, index);
-		arrayrefOfArrayType(o, arrayref);
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        Type arrayref = stack().peek(1);
+        Type index = stack().peek(0);
+
+        indexOfInt(o, index);
+        arrayrefOfArrayType(o, arrayref);
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitCASTORE(CASTORE o){
-		Type arrayref = stack().peek(2);
-		Type index = stack().peek(1);
-		Type value = stack().peek(0);
-		
-		indexOfInt(o, index);
-		valueOfInt(o, value);
-		if (arrayrefOfArrayType(o, arrayref)){
-			if (! ((ArrayType) arrayref).getElementType().equals(Type.CHAR) ){
-				constraintViolated(o, "The 'arrayref' does not refer to an array with elements of type char but to an array of type "+((ArrayType) arrayref).getElementType()+".");
-			}
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        Type arrayref = stack().peek(2);
+        Type index = stack().peek(1);
+        Type value = stack().peek(0);
+
+        indexOfInt(o, index);
+        valueOfInt(o, value);
+        if (arrayrefOfArrayType(o, arrayref)){
+            if (! ((ArrayType) arrayref).getElementType().equals(Type.CHAR) ){
+                constraintViolated(o, "The 'arrayref' does not refer to an array with elements of type char but to an array of type "+((ArrayType) arrayref).getElementType()+".");
+            }
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitCHECKCAST(CHECKCAST o){
-		// The objectref must be of type reference.
-		Type objectref = stack().peek(0);
-		if (!(objectref instanceof ReferenceType)){
-			constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type "+objectref+".");
-		}
-		//else{
-		//	referenceTypeIsInitialized(o, (ReferenceType) objectref);
-		//}
-		// The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
-		// current class (�3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
-		// pool item at the index must be a symbolic reference to a class, array, or interface type.
-		Constant c = cpg.getConstant(o.getIndex());
-		if (! (c instanceof ConstantClass)){
-			constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '"+c+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        // The objectref must be of type reference.
+        Type objectref = stack().peek(0);
+        if (!(objectref instanceof ReferenceType)){
+            constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type "+objectref+".");
+        }
+        //else{
+        //    referenceTypeIsInitialized(o, (ReferenceType) objectref);
+        //}
+        // The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
+        // current class (�3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
+        // pool item at the index must be a symbolic reference to a class, array, or interface type.
+        Constant c = cpg.getConstant(o.getIndex());
+        if (! (c instanceof ConstantClass)){
+            constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '"+c+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitD2F(D2F o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitD2I(D2I o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitD2L(D2L o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDADD(DADD o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDALOAD(DALOAD o){
-		indexOfInt(o, stack().peek());
-		if (stack().peek(1) == Type.NULL){
-			return;
-		} 
-		if (! (stack().peek(1) instanceof ArrayType)){
-			constraintViolated(o, "Stack next-to-top must be of type double[] but is '"+stack().peek(1)+"'.");
-		}
-		Type t = ((ArrayType) (stack().peek(1))).getBasicType();
-		if (t != Type.DOUBLE){
-			constraintViolated(o, "Stack next-to-top must be of type double[] but is '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        indexOfInt(o, stack().peek());
+        if (stack().peek(1) == Type.NULL){
+            return;
+        } 
+        if (! (stack().peek(1) instanceof ArrayType)){
+            constraintViolated(o, "Stack next-to-top must be of type double[] but is '"+stack().peek(1)+"'.");
+        }
+        Type t = ((ArrayType) (stack().peek(1))).getBasicType();
+        if (t != Type.DOUBLE){
+            constraintViolated(o, "Stack next-to-top must be of type double[] but is '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDASTORE(DASTORE o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-		indexOfInt(o, stack().peek(1));
-		if (stack().peek(2) == Type.NULL){
-			return;
-		} 
-		if (! (stack().peek(2) instanceof ArrayType)){
-			constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '"+stack().peek(2)+"'.");
-		}
-		Type t = ((ArrayType) (stack().peek(2))).getBasicType();
-		if (t != Type.DOUBLE){
-			constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '"+stack().peek(2)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+        indexOfInt(o, stack().peek(1));
+        if (stack().peek(2) == Type.NULL){
+            return;
+        } 
+        if (! (stack().peek(2) instanceof ArrayType)){
+            constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '"+stack().peek(2)+"'.");
+        }
+        Type t = ((ArrayType) (stack().peek(2))).getBasicType();
+        if (t != Type.DOUBLE){
+            constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '"+stack().peek(2)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDCMPG(DCMPG o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDCMPL(DCMPL o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDCONST(DCONST o){
-		// There's nothing to be done here.
-	}
-	
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        // There's nothing to be done here.
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDDIV(DDIV o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDLOAD(DLOAD o){
-		//visitLoadInstruction(LoadInstruction) is called before.
-		
-		// Nothing else needs to be done here.
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        //visitLoadInstruction(LoadInstruction) is called before.
+
+        // Nothing else needs to be done here.
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDMUL(DMUL o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDNEG(DNEG o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDREM(DREM o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDRETURN(DRETURN o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDSTORE(DSTORE o){
-		//visitStoreInstruction(StoreInstruction) is called before.
-		
-		// Nothing else needs to be done here.
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        //visitStoreInstruction(StoreInstruction) is called before.
+
+        // Nothing else needs to be done here.
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDSUB(DSUB o){
-		if (stack().peek() != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.DOUBLE){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.DOUBLE){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDUP(DUP o){
-		if (stack().peek().getSize() != 1){
-			constraintViolated(o, "Won't DUP type on stack top '"+stack().peek()+"' because it must occupy exactly one slot, not '"+stack().peek().getSize()+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek().getSize() != 1){
+            constraintViolated(o, "Won't DUP type on stack top '"+stack().peek()+"' because it must occupy exactly one slot, not '"+stack().peek().getSize()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDUP_X1(DUP_X1 o){
-		if (stack().peek().getSize() != 1){
-			constraintViolated(o, "Type on stack top '"+stack().peek()+"' should occupy exactly one slot, not '"+stack().peek().getSize()+"'.");
-		}
-		if (stack().peek(1).getSize() != 1){
-			constraintViolated(o, "Type on stack next-to-top '"+stack().peek(1)+"' should occupy exactly one slot, not '"+stack().peek(1).getSize()+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek().getSize() != 1){
+            constraintViolated(o, "Type on stack top '"+stack().peek()+"' should occupy exactly one slot, not '"+stack().peek().getSize()+"'.");
+        }
+        if (stack().peek(1).getSize() != 1){
+            constraintViolated(o, "Type on stack next-to-top '"+stack().peek(1)+"' should occupy exactly one slot, not '"+stack().peek(1).getSize()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDUP_X2(DUP_X2 o){
-		if (stack().peek().getSize() != 1){
-			constraintViolated(o, "Stack top type must be of size 1, but is '"+stack().peek()+"' of size '"+stack().peek().getSize()+"'.");
-		}
-		if (stack().peek(1).getSize() == 2){
-			return; // Form 2, okay.
-		}
-		else{   //stack().peek(1).getSize == 1.
-			if (stack().peek(2).getSize() != 1){
-				constraintViolated(o, "If stack top's size is 1 and stack next-to-top's size is 1, stack next-to-next-to-top's size must also be 1, but is: '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'.");
-			}
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek().getSize() != 1){
+            constraintViolated(o, "Stack top type must be of size 1, but is '"+stack().peek()+"' of size '"+stack().peek().getSize()+"'.");
+        }
+        if (stack().peek(1).getSize() == 2){
+            return; // Form 2, okay.
+        }
+        else{   //stack().peek(1).getSize == 1.
+            if (stack().peek(2).getSize() != 1){
+                constraintViolated(o, "If stack top's size is 1 and stack next-to-top's size is 1, stack next-to-next-to-top's size must also be 1, but is: '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'.");
+            }
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDUP2(DUP2 o){
-		if (stack().peek().getSize() == 2){
-			return; // Form 2, okay.
-		}
-		else{ //stack().peek().getSize() == 1.
-			if (stack().peek(1).getSize() != 1){
-				constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'.");
-			}
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek().getSize() == 2){
+            return; // Form 2, okay.
+        }
+        else{ //stack().peek().getSize() == 1.
+            if (stack().peek(1).getSize() != 1){
+                constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'.");
+            }
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDUP2_X1(DUP2_X1 o){
-		if (stack().peek().getSize() == 2){
-			if (stack().peek(1).getSize() != 1){
-				constraintViolated(o, "If stack top's size is 2, then stack next-to-top's size must be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'.");
-			}
-			else{
-				return; // Form 2
-			}
-		}
-		else{ // stack top is of size 1
-			if ( stack().peek(1).getSize() != 1 ){
-				constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'.");
-			}
-			if ( stack().peek(2).getSize() != 1 ){
-				constraintViolated(o, "If stack top's size is 1, then stack next-to-next-to-top's size must also be 1. But it is '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'.");
-			}
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek().getSize() == 2){
+            if (stack().peek(1).getSize() != 1){
+                constraintViolated(o, "If stack top's size is 2, then stack next-to-top's size must be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'.");
+            }
+            else{
+                return; // Form 2
+            }
+        }
+        else{ // stack top is of size 1
+            if ( stack().peek(1).getSize() != 1 ){
+                constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '"+stack().peek(1)+"' of size '"+stack().peek(1).getSize()+"'.");
+            }
+            if ( stack().peek(2).getSize() != 1 ){
+                constraintViolated(o, "If stack top's size is 1, then stack next-to-next-to-top's size must also be 1. But it is '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'.");
+            }
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitDUP2_X2(DUP2_X2 o){
 
-		if (stack().peek(0).getSize() == 2){
-		 	if (stack().peek(1).getSize() == 2){
-				return; // Form 4
-			}
-			else{// stack top size is 2, next-to-top's size is 1
-				if ( stack().peek(2).getSize() != 1 ){
-					constraintViolated(o, "If stack top's size is 2 and stack-next-to-top's size is 1, then stack next-to-next-to-top's size must also be 1. But it is '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'.");
-				}
-				else{
-					return; // Form 2
-				}
-			}
-		}
-		else{// stack top is of size 1
-			if (stack().peek(1).getSize() == 1){
-				if ( stack().peek(2).getSize() == 2 ){
-					return; // Form 3
-				}
-				else{
-					if ( stack().peek(3).getSize() == 1){
-						return; // Form 1
-					}
-				}
-			}
-		}
-		constraintViolated(o, "The operand sizes on the stack do not match any of the four forms of usage of this instruction.");
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek(0).getSize() == 2){
+             if (stack().peek(1).getSize() == 2){
+                return; // Form 4
+            }
+            else{// stack top size is 2, next-to-top's size is 1
+                if ( stack().peek(2).getSize() != 1 ){
+                    constraintViolated(o, "If stack top's size is 2 and stack-next-to-top's size is 1, then stack next-to-next-to-top's size must also be 1. But it is '"+stack().peek(2)+"' of size '"+stack().peek(2).getSize()+"'.");
+                }
+                else{
+                    return; // Form 2
+                }
+            }
+        }
+        else{// stack top is of size 1
+            if (stack().peek(1).getSize() == 1){
+                if ( stack().peek(2).getSize() == 2 ){
+                    return; // Form 3
+                }
+                else{
+                    if ( stack().peek(3).getSize() == 1){
+                        return; // Form 1
+                    }
+                }
+            }
+        }
+        constraintViolated(o, "The operand sizes on the stack do not match any of the four forms of usage of this instruction.");
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitF2D(F2D o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitF2I(F2I o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitF2L(F2L o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-	}
-	
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFADD(FADD o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.FLOAT){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.FLOAT){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFALOAD(FALOAD o){
-		indexOfInt(o, stack().peek());
-		if (stack().peek(1) == Type.NULL){
-			return;
-		} 
-		if (! (stack().peek(1) instanceof ArrayType)){
-			constraintViolated(o, "Stack next-to-top must be of type float[] but is '"+stack().peek(1)+"'.");
-		}
-		Type t = ((ArrayType) (stack().peek(1))).getBasicType();
-		if (t != Type.FLOAT){
-			constraintViolated(o, "Stack next-to-top must be of type float[] but is '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        indexOfInt(o, stack().peek());
+        if (stack().peek(1) == Type.NULL){
+            return;
+        } 
+        if (! (stack().peek(1) instanceof ArrayType)){
+            constraintViolated(o, "Stack next-to-top must be of type float[] but is '"+stack().peek(1)+"'.");
+        }
+        Type t = ((ArrayType) (stack().peek(1))).getBasicType();
+        if (t != Type.FLOAT){
+            constraintViolated(o, "Stack next-to-top must be of type float[] but is '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFASTORE(FASTORE o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-		indexOfInt(o, stack().peek(1));
-		if (stack().peek(2) == Type.NULL){
-			return;
-		} 
-		if (! (stack().peek(2) instanceof ArrayType)){
-			constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '"+stack().peek(2)+"'.");
-		}
-		Type t = ((ArrayType) (stack().peek(2))).getBasicType();
-		if (t != Type.FLOAT){
-			constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '"+stack().peek(2)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+        indexOfInt(o, stack().peek(1));
+        if (stack().peek(2) == Type.NULL){
+            return;
+        } 
+        if (! (stack().peek(2) instanceof ArrayType)){
+            constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '"+stack().peek(2)+"'.");
+        }
+        Type t = ((ArrayType) (stack().peek(2))).getBasicType();
+        if (t != Type.FLOAT){
+            constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '"+stack().peek(2)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFCMPG(FCMPG o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.FLOAT){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.FLOAT){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFCMPL(FCMPL o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.FLOAT){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.FLOAT){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFCONST(FCONST o){
-		// nothing to do here.
-	}
+        // nothing to do here.
+    }
 
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFDIV(FDIV o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.FLOAT){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.FLOAT){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFLOAD(FLOAD o){
-		//visitLoadInstruction(LoadInstruction) is called before.
-		
-		// Nothing else needs to be done here.
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        //visitLoadInstruction(LoadInstruction) is called before.
+
+        // Nothing else needs to be done here.
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFMUL(FMUL o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.FLOAT){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.FLOAT){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFNEG(FNEG o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFREM(FREM o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.FLOAT){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.FLOAT){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFRETURN(FRETURN o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFSTORE(FSTORE o){
-		//visitStoreInstruction(StoreInstruction) is called before.
-		
-		// Nothing else needs to be done here.
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        //visitStoreInstruction(StoreInstruction) is called before.
+
+        // Nothing else needs to be done here.
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitFSUB(FSUB o){
-		if (stack().peek() != Type.FLOAT){
-			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
-		}
-		if (stack().peek(1) != Type.FLOAT){
-			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
-		}
-	}
-
-	/**
-	 * Ensures the specific preconditions of the said instruction.
-	 */
-	@Override
+        if (stack().peek() != Type.FLOAT){
+            constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
+        }
+        if (stack().peek(1) != Type.FLOAT){
+            constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
+        }
+    }
+
+    /**
+     * Ensures the specific preconditions of the said instruction.
+     */
+    @Override
     public void visitGETFIELD(GETFIELD o){
-	    try {
-		Type objectref = stack().peek();
-		if (! ( (objectref instanceof ObjectType) || (objectref == Type.NULL) ) ){
-			constraintViolated(o, "Stack top should be an object reference that's not an array reference, but is '"+objectref+"'.");
-		}
-		
-		String field_name = o.getFieldName(cpg);
-		
-		JavaClass jc = Repository.lookupClass(o.getClassType(cpg).getClassName());
-		Field[] fields = jc.getFields();
-		Field f = null;
-		for (Field field : fields) {
-			if (field.getName().equals(field_name)){
-				  Type f_type = Type.getType(field.getSignature());
-				  Type o_type = o.getType(cpg);
-					/* TODO: Check if assignment compatibility is sufficient.
-				   * What does Sun do?
-				   */
-				  if (f_type.equals(o_type)){
-						f = field;
-						break;
-					}
-			}
-		}
-
-		if (f == null){
-			JavaClass[] superclasses = jc.getSuperClasses();
-			outer:
+        try {
+        Type objectref = stack().peek();
+        if (! ( (objectref instanceof ObjectType) || (objectref == Type.NULL) ) ){
+            constraintViolated(o, "Stack top should be an object reference that's not an array reference, but is '"+objectref+"'.");
+        }
+
+        String field_name = o.getFieldName(cpg);
+
+        JavaClass jc = Repository.lookupClass(o.getClassType(cpg).getClassName());
+        Field[] fields = jc.getFields();
+        Field f = null;
+        for (Field field : fields) {
+            if (field.getName().equals(field_name)){
+                  Type f_type = Type.getType(field.getSignature());
+                  Type o_type = o.getType(cpg);
+                    /* TODO: Check if assignment compatibility is sufficient.
+                   * What does Sun do?
+                   */
+                  if (f_type.equals(o_type)){
+                        f = field;
+                        break;
+                    }
+            }
+        }
+
+        if (f == null){
+            JavaClass[] superclasses = jc.getSuperClasses();
+            outer:
             for (JavaClass superclass : superclasses) {
                 fields = superclass.getFields();
                 for (Field field : fields) {
@@ -1269,1616 +1269,1616 @@ public class InstConstraintVisitor exten
                     }
                 }
             }
-			if (f == null) {
+            if (f == null) {
                 throw new AssertionViolatedException("Field '" + field_name + "' not found in " + jc.getClassName());
             }
-		}
+        }
+
+        if (f.isProtected()){
+            ObjectType classtype = o.getClassType(cpg);
+            ObjectType curr = ObjectType.getInstance(mg.getClassName());
+
+            if (    classtype.equals(curr) ||
+                        curr.subclassOf(classtype)    ){
+                Type t = stack().peek();
+                if (t == Type.NULL){
+                    return;
+                }
+                if (! (t instanceof ObjectType) ){
+                    constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '"+t+"'.");
+                }
+                ObjectType objreftype = (ObjectType) t;
+                if (! ( objreftype.equals(curr) ||
+                            objreftype.subclassOf(curr) ) ){
+                    //TODO: One day move to Staerk-et-al's "Set of object types" instead of "wider" object types
+                    //      created during the verification.
+                    //      "Wider" object types don't allow us to check for things like that below.
+                    //constraintViolated(o, "The referenced field has the ACC_PROTECTED modifier, and it's a member of the current class or a superclass of the current class. However, the referenced object type '"+stack().peek()+"' is not the current class or a subclass of the current class.");
+                }
+            } 
+        }
 
-		if (f.isProtected()){
-			ObjectType classtype = o.getClassType(cpg);
-			ObjectType curr = ObjectType.getInstance(mg.getClassName());
-
-			if (	classtype.equals(curr) ||
-						curr.subclassOf(classtype)	){
-				Type t = stack().peek();
-				if (t == Type.NULL){
-					return;
-				}
-				if (! (t instanceof ObjectType) ){
-					constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '"+t+"'.");
-				}
-				ObjectType objreftype = (ObjectType) t;
-				if (! ( objreftype.equals(curr) ||
-						    objreftype.subclassOf(curr) ) ){
-					//TODO: One day move to Staerk-et-al's "Set of object types" instead of "wider" object types

[... 3055 lines stripped ...]


Mime
View raw message