    View Javadoc
    1   package org.apache.bcel.verifier.structurals;
    2
    3   /* ====================================================================
    4    * The Apache Software License, Version 1.1
    5    *
    6    * Copyright (c) 2001 The Apache Software Foundation.  All rights
    7    * reserved.
    8    *
    9    * Redistribution and use in source and binary forms, with or without
    10   * modification, are permitted provided that the following conditions
    11   * are met:
    12   *
    13   * 1. Redistributions of source code must retain the above copyright
    14   *    notice, this list of conditions and the following disclaimer.
    15   *
    16   * 2. Redistributions in binary form must reproduce the above copyright
    17   *    notice, this list of conditions and the following disclaimer in
    18   *    the documentation and/or other materials provided with the
    19   *    distribution.
    20   *
    21   * 3. The end-user documentation included with the redistribution,
    22   *    if any, must include the following acknowledgment:
    23   *       "This product includes software developed by the
    24   *        Apache Software Foundation (http://www.apache.org/)."
    25   *    Alternately, this acknowledgment may appear in the software itself,
    26   *    if and wherever such third-party acknowledgments normally appear.
    27   *
    28   * 4. The names "Apache" and "Apache Software Foundation" and
    29   *    "Apache BCEL" must not be used to endorse or promote products
    30   *    derived from this software without prior written permission. For
    31   *    written permission, please contact apache@apache.org.
    32   *
    33   * 5. Products derived from this software may not be called "Apache",
    34   *    "Apache BCEL", nor may "Apache" appear in their name, without
    35   *    prior written permission of the Apache Software Foundation.
    36   *
    37   * THIS SOFTWARE IS PROVIDED ``AS IS'' AND ANY EXPRESSED OR IMPLIED
    38   * WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
    39   * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
    40   * DISCLAIMED.  IN NO EVENT SHALL THE APACHE SOFTWARE FOUNDATION OR
    41   * ITS CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
    42   * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
    43   * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF
    44   * USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
    45   * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
    46   * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT
    47   * OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
    48   * SUCH DAMAGE.
    49   * ====================================================================
    50   *
    51   * This software consists of voluntary contributions made by many
    52   * individuals on behalf of the Apache Software Foundation.  For more
    53   * information on the Apache Software Foundation, please see
    54   * <http://www.apache.org/>;.
    55   */
    56
    57  import org.apache.bcel.Constants;
    58  import org.apache.bcel.Repository;
    59  import org.apache.bcel.classfile.Constant;
    60  import org.apache.bcel.classfile.ConstantClass;
    61  import org.apache.bcel.classfile.ConstantDouble;
    62  import org.apache.bcel.classfile.ConstantInteger;
    63  import org.apache.bcel.classfile.ConstantFieldref;
    64  import org.apache.bcel.classfile.ConstantFloat;
    65  import org.apache.bcel.classfile.ConstantLong;
    66  import org.apache.bcel.classfile.ConstantString;
    67  import org.apache.bcel.classfile.Field;
    68  import org.apache.bcel.classfile.JavaClass;
    69  import org.apache.bcel.generic.*;
    70  import org.apache.bcel.verifier.*;
    71  import org.apache.bcel.verifier.exc.*;
    72
    73
    74  /***
    75   * A Visitor class testing for valid preconditions of JVM instructions.
    76   * The instance of this class will throw a StructuralCodeConstraintException
    77   * instance if an instruction is visitXXX()ed which has preconditions that are
    78   * not satisfied.
    79   * TODO: Currently, the JVM's behaviour concerning monitors (MONITORENTER,
    80   * MONITOREXIT) is not modeled in JustIce.
    81   *
    82   * @version $Id: InstConstraintVisitor.java,v 1.5 2003/02/12 10:15:29 enver Exp $
    83   * @author <A HREF="http://www.inf.fu-berlin.de/~ehaase"/>Enver Haase</A>
    84   * @see org.apache.bcel.verifier.exc.StructuralCodeConstraintException
    85   * @see org.apache.bcel.verifier.exc.LinkingConstraintException
    86   */
    87  public class InstConstraintVisitor extends EmptyVisitor implements org.apache.bcel.generic.Visitor{
    88
    89  	private static ObjectType GENERIC_ARRAY = new ObjectType("org.apache.bcel.verifier.structurals.GenericArray");
    90
    91  	/***
    92  	 * The constructor. Constructs a new instance of this class.
    93  	 */
    94  	public InstConstraintVisitor(){}
    95
    96  	/***
    97  	 * The Execution Frame we're working on.
    98  	 *
    99  	 * @see #setFrame(Frame f)
    100 	 * @see #locals()
    101 	 * @see #stack()
    102 	 */
    103 	private Frame frame = null;
    104
    105 	/***
    106 	 * The ConstantPoolGen we're working on.
    107 	 *
    108 	 * @see #setConstantPoolGen(ConstantPoolGen cpg)
    109 	 */
    110 	private ConstantPoolGen cpg = null;
    111
    112 	/***
    113 	 * The MethodGen we're working on.
    114 	 *
    115 	 * @see #setMethodGen(MethodGen mg)
    116 	 */
    117 	private MethodGen mg = null;
    118
    119 	/***
    120 	 * The OperandStack we're working on.
    121 	 *
    122 	 * @see #setFrame(Frame f)
    123 	 */
    124 	private OperandStack stack(){
    125 		return frame.getStack();
    126 	}
    127
    128 	/***
    129 	 * The LocalVariables we're working on.
    130 	 *
    131 	 * @see #setFrame(Frame f)
    132 	 */
    133 	private LocalVariables locals(){
    134 		return frame.getLocals();
    135 	}
    136
    137 	/***
    138    * This method is called by the visitXXX() to notify the acceptor of this InstConstraintVisitor
    139    * that a constraint violation has occured. This is done by throwing an instance of a
    140    * StructuralCodeConstraintException.
    141    * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException always.
    142    */
    143 	private void constraintViolated(Instruction violator, String description){
    144 		String fq_classname = violator.getClass().getName();
    145 		throw new StructuralCodeConstraintException("Instruction "+ fq_classname.substring(fq_classname.lastIndexOf('.')+1) +" constraint violated: " + description);
    146 	}
    147
    148 	/***
    149 	 * This returns the single instance of the InstConstraintVisitor class.
    150 	 * To operate correctly, other values must have been set before actually
    151 	 * using the instance.
    152 	 * Use this method for performance reasons.
    153 	 *
    154 	 * @see #setConstantPoolGen(ConstantPoolGen cpg)
    155 	 * @see #setMethodGen(MethodGen mg)
    156 	 */
    157 	public void setFrame(Frame f){
    158 		this.frame = f;
    159 		//if (singleInstance.mg == null || singleInstance.cpg == null) throw new AssertionViolatedException("Forgot to set important values first.");
    160 	}
    161
    162 	/***
    163 	 * Sets the ConstantPoolGen instance needed for constraint
    164 	 * checking prior to execution.
    165 	 */
    166 	public void setConstantPoolGen(ConstantPoolGen cpg){
    167 		this.cpg = cpg;
    168 	}
    169
    170 	/***
    171 	 * Sets the MethodGen instance needed for constraint
    172 	 * checking prior to execution.
    173 	 */
    174 	public void setMethodGen(MethodGen mg){
    175 		this.mg = mg;
    176 	}
    177
    178 	/***
    179 	 * Assures index is of type INT.
    180 	 * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied.
    181 	 */
    182 	private void indexOfInt(Instruction o, Type index){
    183 		if (! index.equals(Type.INT))
    184 				constraintViolated(o, "The 'index' is not of type int but of type "+index+".");
    185 	}
    186
    187 	/***
    188 	 * Assures the ReferenceType r is initialized (or Type.NULL).
    189 	 * Formally, this means (!(r instanceof UninitializedObjectType)), because
    190 	 * there are no uninitialized array types.
    191 	 * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is not satisfied.
    192 	 */
    193 	private void referenceTypeIsInitialized(Instruction o, ReferenceType r){
    194 		if (r instanceof UninitializedObjectType){
    195 			constraintViolated(o, "Working on an uninitialized object '"+r+"'.");
    196 		}
    197 	}
    198
    199 	/*** Assures value is of type INT. */
    200 	private void valueOfInt(Instruction o, Type value){
    201 		if (! value.equals(Type.INT))
    202 				constraintViolated(o, "The 'value' is not of type int but of type "+value+".");
    203 	}
    204
    205 	/***
    206 	 * Assures arrayref is of ArrayType or NULL;
    207 	 * returns true if and only if arrayref is non-NULL.
    208 	 * @throws org.apache.bcel.verifier.exc.StructuralCodeConstraintException if the above constraint is violated.
    209  	 */
    210 	private boolean arrayrefOfArrayType(Instruction o, Type arrayref){
    211 		if (! ((arrayref instanceof ArrayType) || arrayref.equals(Type.NULL)) )
    212 				constraintViolated(o, "The 'arrayref' does not refer to an array but is of type "+arrayref+".");
    213 		return (arrayref instanceof ArrayType);
    214 	}
    215
    216 	/****************************************************************/
    217 	/* MISC                                                        */
    218 	/****************************************************************/
    219 	/***
    220 	 * Ensures the general preconditions of an instruction that accesses the stack.
    221 	 * This method is here because BCEL has no such superinterface for the stack
    222 	 * accessing instructions; and there are funny unexpected exceptions in the
    223 	 * semantices of the superinterfaces and superclasses provided.
    224 	 * E.g. SWAP is a StackConsumer, but DUP_X1 is not a StackProducer.
    225 	 * Therefore, this method is called by all StackProducer, StackConsumer,
    226 	 * and StackInstruction instances via their visitXXX() method.
    227 	 * Unfortunately, as the superclasses and superinterfaces overlap, some instructions
    228 	 * cause this method to be called two or three times. [TODO: Fix this.]
    229 	 *
    230 	 * @see #visitStackConsumer(StackConsumer o)
    231 	 * @see #visitStackProducer(StackProducer o)
    232 	 * @see #visitStackInstruction(StackInstruction o)
    233 	 */
    234 	private void _visitStackAccessor(Instruction o){
    235 		int consume = o.consumeStack(cpg); // Stack values are always consumed first; then produced.
    236 		if (consume > stack().slotsUsed()){
    237 			constraintViolated((Instruction) o, "Cannot consume "+consume+" stack slots: only "+stack().slotsUsed()+" slot(s) left on stack!\nStack:\n"+stack());
    238 		}
    239
    240 		int produce = o.produceStack(cpg) - ((Instruction) o).consumeStack(cpg); // Stack values are always consumed first; then produced.
    241 		if ( produce + stack().slotsUsed() > stack().maxStack() ){
    242 			constraintViolated((Instruction) o, "Cannot produce "+produce+" stack slots: only "+(stack().maxStack()-stack().slotsUsed())+" free stack slot(s) left.\nStack:\n"+stack());
    243 		}
    244 	}
    245
    246 	/****************************************************************/
    247 	/* "generic"visitXXXX methods where XXXX is an interface       */
    248 	/* therefore, we don't know the order of visiting; but we know */
    249 	/* these methods are called before the visitYYYY methods below */
    250 	/****************************************************************/
    251
    252 	/***
    253 	 * Assures the generic preconditions of a LoadClass instance.
    254 	 * The referenced class is loaded and pass2-verified.
    255 	 */
    256 	public void visitLoadClass(LoadClass o){
    257 		ObjectType t = o.getLoadClassType(cpg);
    258 		if (t != null){// null means "no class is loaded"
    259 			Verifier v = VerifierFactory.getVerifier(t.getClassName());
    260 			VerificationResult vr = v.doPass2();
    261 			if (vr.getStatus() != VerificationResult.VERIFIED_OK){
    262 				constraintViolated((Instruction) o, "Class '"+o.getLoadClassType(cpg).getClassName()+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
    263 			}
    264 		}
    265 	}
    266
    267 	/***
    268 	 * Ensures the general preconditions of a StackConsumer instance.
    269 	 */
    270 	public void visitStackConsumer(StackConsumer o){
    271 		_visitStackAccessor((Instruction) o);
    272 	}
    273
    274 	/***
    275 	 * Ensures the general preconditions of a StackProducer instance.
    276 	 */
    277 	public void visitStackProducer(StackProducer o){
    278 		_visitStackAccessor((Instruction) o);
    279 	}
    280
    281
    282 	/****************************************************************/
    283 	/* "generic" visitYYYY methods where YYYY is a superclass.     */
    284 	/* therefore, we know the order of visiting; we know           */
    285 	/* these methods are called after the visitXXXX methods above. */
    286 	/****************************************************************/
    287 	/***
    288 	 * Ensures the general preconditions of a CPInstruction instance.
    289 	 */
    290 	public void visitCPInstruction(CPInstruction o){
    291 		int idx = o.getIndex();
    292 		if ((idx < 0) || (idx >= cpg.getSize())){
    293 			throw new AssertionViolatedException("Huh?! Constant pool index of instruction '"+o+"' illegal? Pass 3a should have checked this!");
    294 		}
    295 	}
    296
    297 	/***
    298 	 * Ensures the general preconditions of a FieldInstruction instance.
    299 	 */
    300 	 public void visitFieldInstruction(FieldInstruction o){
    301 	 	// visitLoadClass(o) has been called before: Every FieldOrMethod
    302 	 	// implements LoadClass.
    303 	 	// visitCPInstruction(o) has been called before.
    304 		// A FieldInstruction may be: GETFIELD, GETSTATIC, PUTFIELD, PUTSTATIC
    305 			Constant c = cpg.getConstant(o.getIndex());
    306 			if (!(c instanceof ConstantFieldref)){
    307 				constraintViolated(o, "Index '"+o.getIndex()+"' should refer to a CONSTANT_Fieldref_info structure, but refers to '"+c+"'.");
    308 			}
    309 			// the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
    310 			Type t = o.getType(cpg);
    311 			if (t instanceof ObjectType){
    312 				String name = ((ObjectType)t).getClassName();
    313 				Verifier v = VerifierFactory.getVerifier( name );
    314 				VerificationResult vr = v.doPass2();
    315 				if (vr.getStatus() != VerificationResult.VERIFIED_OK){
    316 					constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
    317 				}
    318 			}
    319 	 }
    320
    321 	/***
    322 	 * Ensures the general preconditions of an InvokeInstruction instance.
    323 	 */
    324 	 public void visitInvokeInstruction(InvokeInstruction o){
    325 	 	// visitLoadClass(o) has been called before: Every FieldOrMethod
    326 	 	// implements LoadClass.
    327 	 	// visitCPInstruction(o) has been called before.
    328         //TODO
    329 	 }
    330
    331 	/***
    332 	 * Ensures the general preconditions of a StackInstruction instance.
    333 	 */
    334 	public void visitStackInstruction(StackInstruction o){
    335 		_visitStackAccessor(o);
    336 	}
    337
    338 	/***
    339 	 * Assures the generic preconditions of a LocalVariableInstruction instance.
    340 	 * That is, the index of the local variable must be valid.
    341 	 */
    342 	public void visitLocalVariableInstruction(LocalVariableInstruction o){
    343 		if (locals().maxLocals() <= (o.getType(cpg).getSize()==1? o.getIndex() : o.getIndex()+1) ){
    344 			constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
    345 		}
    346 	}
    347
    348 	/***
    349 	 * Assures the generic preconditions of a LoadInstruction instance.
    350 	 */
    351 	public void visitLoadInstruction(LoadInstruction o){
    352 		//visitLocalVariableInstruction(o) is called before, because it is more generic.
    353
    354 		// LOAD instructions must not read Type.UNKNOWN
    355 		if (locals().get(o.getIndex()) == Type.UNKNOWN){
    356 			constraintViolated(o, "Read-Access on local variable "+o.getIndex()+" with unknown content.");
    357 		}
    358
    359 		// LOAD instructions, two-slot-values at index N must have Type.UNKNOWN
    360 		// as a symbol for the higher halve at index N+1
    361 		// [suppose some instruction put an int at N+1--- our double at N is defective]
    362 		if (o.getType(cpg).getSize() == 2){
    363 			if (locals().get(o.getIndex()+1) != Type.UNKNOWN){
    364 				constraintViolated(o, "Reading a two-locals value from local variables "+o.getIndex()+" and "+(o.getIndex()+1)+" where the latter one is destroyed.");
    365 			}
    366 		}
    367
    368 		// LOAD instructions must read the correct type.
    369 		if (!(o instanceof ALOAD)){
    370 			if (locals().get(o.getIndex()) != o.getType(cpg) ){
    371 				constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction type: '"+o.getType(cpg)+"'.");
    372 			}
    373 		}
    374 		else{ // we deal with an ALOAD
    375 			if (!(locals().get(o.getIndex()) instanceof ReferenceType)){
    376 				constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '"+locals().get(o.getIndex())+"'; Instruction expects a ReferenceType.");
    377 			}
    378 			// ALOAD __IS ALLOWED__ to put uninitialized objects onto the stack!
    379 			//referenceTypeIsInitialized(o, (ReferenceType) (locals().get(o.getIndex())));
    380 		}
    381
    382 		// LOAD instructions must have enough free stack slots.
    383 		if ((stack().maxStack() - stack().slotsUsed()) < o.getType(cpg).getSize()){
    384 			constraintViolated(o, "Not enough free stack slots to load a '"+o.getType(cpg)+"' onto the OperandStack.");
    385 		}
    386 	}
    387
    388 	/***
    389 	 * Assures the generic preconditions of a StoreInstruction instance.
    390 	 */
    391 	public void visitStoreInstruction(StoreInstruction o){
    392 		//visitLocalVariableInstruction(o) is called before, because it is more generic.
    393
    394 		if (stack().isEmpty()){ // Don't bother about 1 or 2 stack slots used. This check is implicitely done below while type checking.
    395 			constraintViolated(o, "Cannot STORE: Stack to read from is empty.");
    396 		}
    397
    398 		if ( (!(o instanceof ASTORE)) ){
    399 			if (! (stack().peek() == o.getType(cpg)) ){// the other xSTORE types are singletons in BCEL.
    400 				constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction type: '"+o.getType(cpg)+"'.");
    401 			}
    402 		}
    403 		else{ // we deal with ASTORE
    404 			Type stacktop = stack().peek();
    405 			if ( (!(stacktop instanceof ReferenceType)) && (!(stacktop instanceof ReturnaddressType)) ){
    406 				constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '"+stack().peek()+"'; Instruction expects a ReferenceType or a ReturnadressType.");
    407 			}
    408 			if (stacktop instanceof ReferenceType){
    409 				referenceTypeIsInitialized(o, (ReferenceType) stacktop);
    410 			}
    411 		}
    412 	}
    413
    414 	/***
    415 	 * Assures the generic preconditions of a ReturnInstruction instance.
    416 	 */
    417 	public void visitReturnInstruction(ReturnInstruction o){
    418 		if (o instanceof RETURN){
    419 			return;
    420 		}
    421 		if (o instanceof ARETURN){
    422 			if (stack().peek() == Type.NULL){
    423 				return;
    424 			}
    425 			else{
    426 				if (! (stack().peek() instanceof ReferenceType)){
    427 					constraintViolated(o, "Reference type expected on top of stack, but is: '"+stack().peek()+"'.");
    428 				}
    429 				referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()));
    430 				//ReferenceType objectref = (ReferenceType) (stack().peek());
    431 				// TODO: This can only be checked if using Staerk-et-al's "set of object types" instead of a
    432 				// "wider cast object type" created during verification.
    433 				//if (! (objectref.isAssignmentCompatibleWith(mg.getType())) ){
    434 				//	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()+"'.");
    435 				//}
    436 			}
    437 		}
    438 		else{
    439 			Type method_type = mg.getType();
    440 			if (method_type == Type.BOOLEAN ||
    441 					method_type == Type.BYTE ||
    442 					method_type == Type.SHORT ||
    443 					method_type == Type.CHAR){
    444 				method_type = Type.INT;
    445 			}
    446 			if (! ( method_type.equals( stack().peek() ))){
    447 				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()+"'.");
    448 			}
    449 		}
    450 	}
    451
    452 	/****************************************************************/
    453 	/* "special"visitXXXX methods for one type of instruction each */
    454 	/****************************************************************/
    455
    456 	/***
    457 	 * Ensures the specific preconditions of the said instruction.
    458 	 */
    459 	public void visitAALOAD(AALOAD o){
    460 		Type arrayref = stack().peek(1);
    461 		Type index    = stack().peek(0);
    462
    463 		indexOfInt(o, index);
    464 		if (arrayrefOfArrayType(o, arrayref)){
    465 			if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){
    466 				constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+".");
    467 			}
    468 			referenceTypeIsInitialized(o, (ReferenceType) (((ArrayType) arrayref).getElementType()));
    469 		}
    470 	}
    471
    472 	/***
    473 	 * Ensures the specific preconditions of the said instruction.
    474 	 */
    475 	public void visitAASTORE(AASTORE o){
    476 		Type arrayref = stack().peek(2);
    477 		Type index    = stack().peek(1);
    478 		Type value    = stack().peek(0);
    479
    480 		indexOfInt(o, index);
    481 		if (!(value instanceof ReferenceType)){
    482 			constraintViolated(o, "The 'value' is not of a ReferenceType but of type "+value+".");
    483 		}else{
    484 			referenceTypeIsInitialized(o, (ReferenceType) value);
    485 		}
    486 		// Don't bother further with "referenceTypeIsInitialized()", there are no arrays
    487 		// of an uninitialized object type.
    488 		if (arrayrefOfArrayType(o, arrayref)){
    489 			if (! (((ArrayType) arrayref).getElementType() instanceof ReferenceType)){
    490 				constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "+((ArrayType) arrayref).getElementType()+".");
    491 			}
    492 			if (! ((ReferenceType)value).isAssignmentCompatibleWith((ReferenceType) ((ArrayType) arrayref).getElementType())){
    493 				constraintViolated(o, "The type of 'value' ('"+value+"') is not assignment compatible to the components of the array 'arrayref' refers to. ('"+((ArrayType) arrayref).getElementType()+"')");
    494 			}
    495 		}
    496 	}
    497
    498 	/***
    499 	 * Ensures the specific preconditions of the said instruction.
    500 	 */
    501 	public void visitACONST_NULL(ACONST_NULL o){
    502 		// Nothing needs to be done here.
    503 	}
    504
    505 	/***
    506 	 * Ensures the specific preconditions of the said instruction.
    507 	 */
    508 	public void visitALOAD(ALOAD o){
    509 		//visitLoadInstruction(LoadInstruction) is called before.
    510
    511 		// Nothing else needs to be done here.
    512 	}
    513
    514 	/***
    515 	 * Ensures the specific preconditions of the said instruction.
    516 	 */
    517 	public void visitANEWARRAY(ANEWARRAY o){
    518 		if (!stack().peek().equals(Type.INT))
    519 			constraintViolated(o, "The 'count' at the stack top is not of type '"+Type.INT+"' but of type '"+stack().peek()+"'.");
    520 		// The runtime constant pool item at that index must be a symbolic reference to a class,
    521 		// array, or interface type. See Pass 3a.
    522 	}
    523
    524 	/***
    525 	 * Ensures the specific preconditions of the said instruction.
    526 	 */
    527 	public void visitARETURN(ARETURN o){
    528 		if (! (stack().peek() instanceof ReferenceType) ){
    529 			constraintViolated(o, "The 'objectref' at the stack top is not of a ReferenceType but of type '"+stack().peek()+"'.");
    530 		}
    531 		ReferenceType objectref = (ReferenceType) (stack().peek());
    532 		referenceTypeIsInitialized(o, objectref);
    533
    534 		// The check below should already done via visitReturnInstruction(ReturnInstruction), see there.
    535 		// It cannot be done using Staerk-et-al's "set of object types" instead of a
    536 		// "wider cast object type", anyway.
    537 		//if (! objectref.isAssignmentCompatibleWith(mg.getReturnType() )){
    538 		//	constraintViolated(o, "The 'objectref' type "+objectref+" at the stack top is not assignment compatible with the return type '"+mg.getReturnType()+"' of the method.");
    539 		//}
    540 	}
    541
    542 	/***
    543 	 * Ensures the specific preconditions of the said instruction.
    544 	 */
    545 	public void visitARRAYLENGTH(ARRAYLENGTH o){
    546 		Type arrayref = stack().peek(0);
    547 		arrayrefOfArrayType(o, arrayref);
    548 	}
    549
    550 	/***
    551 	 * Ensures the specific preconditions of the said instruction.
    552 	 */
    553 	public void visitASTORE(ASTORE o){
    554 		if (! ( (stack().peek() instanceof ReferenceType) || (stack().peek() instanceof ReturnaddressType) ) ){
    555 			constraintViolated(o, "The 'objectref' is not of a ReferenceType or of ReturnaddressType but of "+stack().peek()+".");
    556 		}
    557 		if (stack().peek() instanceof ReferenceType){
    558 			referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    559 		}
    560 	}
    561
    562 	/***
    563 	 * Ensures the specific preconditions of the said instruction.
    564 	 */
    565 	public void visitATHROW(ATHROW o){
    566 		// It's stated that 'objectref' must be of a ReferenceType --- but since Throwable is
    567 		// not derived from an ArrayType, it follows that 'objectref' must be of an ObjectType or Type.NULL.
    568 		if (! ((stack().peek() instanceof ObjectType) || (stack().peek().equals(Type.NULL))) ){
    569 			constraintViolated(o, "The 'objectref' is not of an (initialized) ObjectType but of type "+stack().peek()+".");
    570 		}
    571
    572 		// NULL is a subclass of every class, so to speak.
    573 		if (stack().peek().equals(Type.NULL)) return;
    574
    575 		ObjectType exc = (ObjectType) (stack().peek());
    576 		ObjectType throwable = (ObjectType) (Type.getType("Ljava/lang/Throwable;"));
    577 		if ( (! (exc.subclassOf(throwable)) ) && (! (exc.equals(throwable))) ){
    578 			constraintViolated(o, "The 'objectref' is not of class Throwable or of a subclass of Throwable, but of '"+stack().peek()+"'.");
    579 		}
    580 	}
    581
    582 	/***
    583 	 * Ensures the specific preconditions of the said instruction.
    584 	 */
    585 	public void visitBALOAD(BALOAD o){
    586 		Type arrayref = stack().peek(1);
    587 		Type index    = stack().peek(0);
    588 		indexOfInt(o, index);
    589 		if (arrayrefOfArrayType(o, arrayref)){
    590 			if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
    591 		 	       (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) ){
    592 				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()+"'.");
    593 			}
    594 		}
    595 	}
    596
    597 	/***
    598 	 * Ensures the specific preconditions of the said instruction.
    599 	 */
    600 	public void visitBASTORE(BASTORE o){
    601 		Type arrayref = stack().peek(2);
    602 		Type index    = stack().peek(1);
    603 		Type value    = stack().peek(0);
    604
    605 		indexOfInt(o, index);
    606 		valueOfInt(o, value);
    607 		if (arrayrefOfArrayType(o, arrayref)){
    608 			if (! ( (((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN)) ||
    609 			        (((ArrayType) arrayref).getElementType().equals(Type.BYTE)) ) )
    610 					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()+"'.");
    611 		}
    612 	}
    613
    614 	/***
    615 	 * Ensures the specific preconditions of the said instruction.
    616 	 */
    617 	public void visitBIPUSH(BIPUSH o){
    618 		// Nothing to do...
    619 	}
    620
    621 	/***
    622 	 * Ensures the specific preconditions of the said instruction.
    623 	 */
    624 	public void visitBREAKPOINT(BREAKPOINT o){
    625 		throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as BREAKPOINT.");
    626 	}
    627
    628 	/***
    629 	 * Ensures the specific preconditions of the said instruction.
    630 	 */
    631 	public void visitCALOAD(CALOAD o){
    632 		Type arrayref = stack().peek(1);
    633 		Type index = stack().peek(0);
    634
    635 		indexOfInt(o, index);
    636 		arrayrefOfArrayType(o, arrayref);
    637 	}
    638
    639 	/***
    640 	 * Ensures the specific preconditions of the said instruction.
    641 	 */
    642 	public void visitCASTORE(CASTORE o){
    643 		Type arrayref = stack().peek(2);
    644 		Type index = stack().peek(1);
    645 		Type value = stack().peek(0);
    646
    647 		indexOfInt(o, index);
    648 		valueOfInt(o, value);
    649 		if (arrayrefOfArrayType(o, arrayref)){
    650 			if (! ((ArrayType) arrayref).getElementType().equals(Type.CHAR) ){
    651 				constraintViolated(o, "The 'arrayref' does not refer to an array with elements of type char but to an array of type "+((ArrayType) arrayref).getElementType()+".");
    652 			}
    653 		}
    654 	}
    655
    656 	/***
    657 	 * Ensures the specific preconditions of the said instruction.
    658 	 */
    659 	public void visitCHECKCAST(CHECKCAST o){
    660 		// The objectref must be of type reference.
    661 		Type objectref = stack().peek(0);
    662 		if (!(objectref instanceof ReferenceType)){
    663 			constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type "+objectref+".");
    664 		}
    665 		else{
    666 			referenceTypeIsInitialized(o, (ReferenceType) objectref);
    667 		}
    668 		// The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
    669 		// current class (§3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
    670 		// pool item at the index must be a symbolic reference to a class, array, or interface type.
    671 		Constant c = cpg.getConstant(o.getIndex());
    672 		if (! (c instanceof ConstantClass)){
    673 			constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '"+c+"'.");
    674 		}
    675 	}
    676
    677 	/***
    678 	 * Ensures the specific preconditions of the said instruction.
    679 	 */
    680 	public void visitD2F(D2F o){
    681 		if (stack().peek() != Type.DOUBLE){
    682 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    683 		}
    684 	}
    685
    686 	/***
    687 	 * Ensures the specific preconditions of the said instruction.
    688 	 */
    689 	public void visitD2I(D2I o){
    690 		if (stack().peek() != Type.DOUBLE){
    691 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    692 		}
    693 	}
    694
    695 	/***
    696 	 * Ensures the specific preconditions of the said instruction.
    697 	 */
    698 	public void visitD2L(D2L o){
    699 		if (stack().peek() != Type.DOUBLE){
    700 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    701 		}
    702 	}
    703
    704 	/***
    705 	 * Ensures the specific preconditions of the said instruction.
    706 	 */
    707 	public void visitDADD(DADD o){
    708 		if (stack().peek() != Type.DOUBLE){
    709 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    710 		}
    711 		if (stack().peek(1) != Type.DOUBLE){
    712 			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
    713 		}
    714 	}
    715
    716 	/***
    717 	 * Ensures the specific preconditions of the said instruction.
    718 	 */
    719 	public void visitDALOAD(DALOAD o){
    720 		indexOfInt(o, stack().peek());
    721 		if (stack().peek(1) == Type.NULL){
    722 			return;
    723 		}
    724 		if (! (stack().peek(1) instanceof ArrayType)){
    725 			constraintViolated(o, "Stack next-to-top must be of type double[] but is '"+stack().peek(1)+"'.");
    726 		}
    727 		Type t = ((ArrayType) (stack().peek(1))).getBasicType();
    728 		if (t != Type.DOUBLE){
    729 			constraintViolated(o, "Stack next-to-top must be of type double[] but is '"+stack().peek(1)+"'.");
    730 		}
    731 	}
    732
    733 	/***
    734 	 * Ensures the specific preconditions of the said instruction.
    735 	 */
    736 	public void visitDASTORE(DASTORE o){
    737 		if (stack().peek() != Type.DOUBLE){
    738 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    739 		}
    740 		indexOfInt(o, stack().peek(1));
    741 		if (stack().peek(2) == Type.NULL){
    742 			return;
    743 		}
    744 		if (! (stack().peek(2) instanceof ArrayType)){
    745 			constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '"+stack().peek(2)+"'.");
    746 		}
    747 		Type t = ((ArrayType) (stack().peek(2))).getBasicType();
    748 		if (t != Type.DOUBLE){
    749 			constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '"+stack().peek(2)+"'.");
    750 		}
    751 	}
    752
    753 	/***
    754 	 * Ensures the specific preconditions of the said instruction.
    755 	 */
    756 	public void visitDCMPG(DCMPG o){
    757 		if (stack().peek() != Type.DOUBLE){
    758 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    759 		}
    760 		if (stack().peek(1) != Type.DOUBLE){
    761 			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
    762 		}
    763 	}
    764
    765 	/***
    766 	 * Ensures the specific preconditions of the said instruction.
    767 	 */
    768 	public void visitDCMPL(DCMPL o){
    769 		if (stack().peek() != Type.DOUBLE){
    770 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    771 		}
    772 		if (stack().peek(1) != Type.DOUBLE){
    773 			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
    774 		}
    775 	}
    776
    777 	/***
    778 	 * Ensures the specific preconditions of the said instruction.
    779 	 */
    780 	public void visitDCONST(DCONST o){
    781 		// There's nothing to be done here.
    782 	}
    783
    784 	/***
    785 	 * Ensures the specific preconditions of the said instruction.
    786 	 */
    787 	public void visitDDIV(DDIV o){
    788 		if (stack().peek() != Type.DOUBLE){
    789 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    790 		}
    791 		if (stack().peek(1) != Type.DOUBLE){
    792 			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
    793 		}
    794 	}
    795
    796 	/***
    797 	 * Ensures the specific preconditions of the said instruction.
    798 	 */
    799 	public void visitDLOAD(DLOAD o){
    800 		//visitLoadInstruction(LoadInstruction) is called before.
    801
    802 		// Nothing else needs to be done here.
    803 	}
    804
    805 	/***
    806 	 * Ensures the specific preconditions of the said instruction.
    807 	 */
    808 	public void visitDMUL(DMUL o){
    809 		if (stack().peek() != Type.DOUBLE){
    810 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    811 		}
    812 		if (stack().peek(1) != Type.DOUBLE){
    813 			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
    814 		}
    815 	}
    816
    817 	/***
    818 	 * Ensures the specific preconditions of the said instruction.
    819 	 */
    820 	public void visitDNEG(DNEG o){
    821 		if (stack().peek() != Type.DOUBLE){
    822 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    823 		}
    824 	}
    825
    826 	/***
    827 	 * Ensures the specific preconditions of the said instruction.
    828 	 */
    829 	public void visitDREM(DREM o){
    830 		if (stack().peek() != Type.DOUBLE){
    831 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    832 		}
    833 		if (stack().peek(1) != Type.DOUBLE){
    834 			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
    835 		}
    836 	}
    837
    838 	/***
    839 	 * Ensures the specific preconditions of the said instruction.
    840 	 */
    841 	public void visitDRETURN(DRETURN o){
    842 		if (stack().peek() != Type.DOUBLE){
    843 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    844 		}
    845 	}
    846
    847 	/***
    848 	 * Ensures the specific preconditions of the said instruction.
    849 	 */
    850 	public void visitDSTORE(DSTORE o){
    851 		//visitStoreInstruction(StoreInstruction) is called before.
    852
    853 		// Nothing else needs to be done here.
    854 	}
    855
    856 	/***
    857 	 * Ensures the specific preconditions of the said instruction.
    858 	 */
    859 	public void visitDSUB(DSUB o){
    860 		if (stack().peek() != Type.DOUBLE){
    861 			constraintViolated(o, "The value at the stack top is not of type 'double', but of type '"+stack().peek()+"'.");
    862 		}
    863 		if (stack().peek(1) != Type.DOUBLE){
    864 			constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '"+stack().peek(1)+"'.");
    865 		}
    866 	}
    867
    868 	/***
    869 	 * Ensures the specific preconditions of the said instruction.
    870 	 */
    871 	public void visitDUP(DUP o){
    872 		if (stack().peek().getSize() != 1){
    873 			constraintViolated(o, "Won't DUP type on stack top '"+stack().peek()+"' because it must occupy exactly one slot, not '"+stack().peek().getSize()+"'.");
    874 		}
    875 	}
    876
    877 	/***
    878 	 * Ensures the specific preconditions of the said instruction.
    879 	 */
    880 	public void visitDUP_X1(DUP_X1 o){
    881 		if (stack().peek().getSize() != 1){
    882 			constraintViolated(o, "Type on stack top '"+stack().peek()+"' should occupy exactly one slot, not '"+stack().peek().getSize()+"'.");
    883 		}
    884 		if (stack().peek(1).getSize() != 1){
    885 			constraintViolated(o, "Type on stack next-to-top '"+stack().peek(1)+"' should occupy exactly one slot, not '"+stack().peek(1).getSize()+"'.");
    886 		}
    887 	}
    888
    889 	/***
    890 	 * Ensures the specific preconditions of the said instruction.
    891 	 */
    892 	public void visitDUP_X2(DUP_X2 o){
    893 		if (stack().peek().getSize() != 1){
    894 			constraintViolated(o, "Stack top type must be of size 1, but is '"+stack().peek()+"' of size '"+stack().peek().getSize()+"'.");
    895 		}
    896 		if (stack().peek(1).getSize() == 2){
    897 			return; // Form 2, okay.
    898 		}
    899 		else{   //stack().peek(1).getSize == 1.
    900 			if (stack().peek(2).getSize() != 1){
    901 				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()+"'.");
    902 			}
    903 		}
    904 	}
    905
    906 	/***
    907 	 * Ensures the specific preconditions of the said instruction.
    908 	 */
    909 	public void visitDUP2(DUP2 o){
    910 		if (stack().peek().getSize() == 2){
    911 			return; // Form 2, okay.
    912 		}
    913 		else{ //stack().peek().getSize() == 1.
    914 			if (stack().peek(1).getSize() != 1){
    915 				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()+"'.");
    916 			}
    917 		}
    918 	}
    919
    920 	/***
    921 	 * Ensures the specific preconditions of the said instruction.
    922 	 */
    923 	public void visitDUP2_X1(DUP2_X1 o){
    924 		if (stack().peek().getSize() == 2){
    925 			if (stack().peek(1).getSize() != 1){
    926 				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()+"'.");
    927 			}
    928 			else{
    929 				return; // Form 2
    930 			}
    931 		}
    932 		else{ // stack top is of size 1
    933 			if ( stack().peek(1).getSize() != 1 ){
    934 				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()+"'.");
    935 			}
    936 			if ( stack().peek(2).getSize() != 1 ){
    937 				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()+"'.");
    938 			}
    939 		}
    940 	}
    941
    942 	/***
    943 	 * Ensures the specific preconditions of the said instruction.
    944 	 */
    945 	public void visitDUP2_X2(DUP2_X2 o){
    946
    947 		if (stack().peek(0).getSize() == 2){
    948 		 	if (stack().peek(1).getSize() == 2){
    949 				return; // Form 4
    950 			}
    951 			else{// stack top size is 2, next-to-top's size is 1
    952 				if ( stack().peek(2).getSize() != 1 ){
    953 					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()+"'.");
    954 				}
    955 				else{
    956 					return; // Form 2
    957 				}
    958 			}
    959 		}
    960 		else{// stack top is of size 1
    961 			if (stack().peek(1).getSize() == 1){
    962 				if ( stack().peek(2).getSize() == 2 ){
    963 					return; // Form 3
    964 				}
    965 				else{
    966 					if ( stack().peek(3).getSize() == 1){
    967 						return; // Form 1
    968 					}
    969 				}
    970 			}
    971 		}
    972 		constraintViolated(o, "The operand sizes on the stack do not match any of the four forms of usage of this instruction.");
    973 	}
    974
    975 	/***
    976 	 * Ensures the specific preconditions of the said instruction.
    977 	 */
    978 	public void visitF2D(F2D o){
    979 		if (stack().peek() != Type.FLOAT){
    980 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    981 		}
    982 	}
    983
    984 	/***
    985 	 * Ensures the specific preconditions of the said instruction.
    986 	 */
    987 	public void visitF2I(F2I o){
    988 		if (stack().peek() != Type.FLOAT){
    989 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    990 		}
    991 	}
    992
    993 	/***
    994 	 * Ensures the specific preconditions of the said instruction.
    995 	 */
    996 	public void visitF2L(F2L o){
    997 		if (stack().peek() != Type.FLOAT){
    998 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    999 		}
    1000 	}
    1001
    1002 	/***
    1003 	 * Ensures the specific preconditions of the said instruction.
    1004 	 */
    1005 	public void visitFADD(FADD o){
    1006 		if (stack().peek() != Type.FLOAT){
    1007 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    1008 		}
    1009 		if (stack().peek(1) != Type.FLOAT){
    1010 			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
    1011 		}
    1012 	}
    1013
    1014 	/***
    1015 	 * Ensures the specific preconditions of the said instruction.
    1016 	 */
    1017 	public void visitFALOAD(FALOAD o){
    1018 		indexOfInt(o, stack().peek());
    1019 		if (stack().peek(1) == Type.NULL){
    1020 			return;
    1021 		}
    1022 		if (! (stack().peek(1) instanceof ArrayType)){
    1023 			constraintViolated(o, "Stack next-to-top must be of type float[] but is '"+stack().peek(1)+"'.");
    1024 		}
    1025 		Type t = ((ArrayType) (stack().peek(1))).getBasicType();
    1026 		if (t != Type.FLOAT){
    1027 			constraintViolated(o, "Stack next-to-top must be of type float[] but is '"+stack().peek(1)+"'.");
    1028 		}
    1029 	}
    1030
    1031 	/***
    1032 	 * Ensures the specific preconditions of the said instruction.
    1033 	 */
    1034 	public void visitFASTORE(FASTORE o){
    1035 		if (stack().peek() != Type.FLOAT){
    1036 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    1037 		}
    1038 		indexOfInt(o, stack().peek(1));
    1039 		if (stack().peek(2) == Type.NULL){
    1040 			return;
    1041 		}
    1042 		if (! (stack().peek(2) instanceof ArrayType)){
    1043 			constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '"+stack().peek(2)+"'.");
    1044 		}
    1045 		Type t = ((ArrayType) (stack().peek(2))).getBasicType();
    1046 		if (t != Type.FLOAT){
    1047 			constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '"+stack().peek(2)+"'.");
    1048 		}
    1049 	}
    1050
    1051 	/***
    1052 	 * Ensures the specific preconditions of the said instruction.
    1053 	 */
    1054 	public void visitFCMPG(FCMPG o){
    1055 		if (stack().peek() != Type.FLOAT){
    1056 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    1057 		}
    1058 		if (stack().peek(1) != Type.FLOAT){
    1059 			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
    1060 		}
    1061 	}
    1062
    1063 	/***
    1064 	 * Ensures the specific preconditions of the said instruction.
    1065 	 */
    1066 	public void visitFCMPL(FCMPL o){
    1067 		if (stack().peek() != Type.FLOAT){
    1068 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    1069 		}
    1070 		if (stack().peek(1) != Type.FLOAT){
    1071 			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
    1072 		}
    1073 	}
    1074
    1075 	/***
    1076 	 * Ensures the specific preconditions of the said instruction.
    1077 	 */
    1078 	public void visitFCONST(FCONST o){
    1079 		// nothing to do here.
    1080 	}
    1081
    1082 	/***
    1083 	 * Ensures the specific preconditions of the said instruction.
    1084 	 */
    1085 	public void visitFDIV(FDIV o){
    1086 		if (stack().peek() != Type.FLOAT){
    1087 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    1088 		}
    1089 		if (stack().peek(1) != Type.FLOAT){
    1090 			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
    1091 		}
    1092 	}
    1093
    1094 	/***
    1095 	 * Ensures the specific preconditions of the said instruction.
    1096 	 */
    1097 	public void visitFLOAD(FLOAD o){
    1098 		//visitLoadInstruction(LoadInstruction) is called before.
    1099
    1100 		// Nothing else needs to be done here.
    1101 	}
    1102
    1103 	/***
    1104 	 * Ensures the specific preconditions of the said instruction.
    1105 	 */
    1106 	public void visitFMUL(FMUL o){
    1107 		if (stack().peek() != Type.FLOAT){
    1108 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    1109 		}
    1110 		if (stack().peek(1) != Type.FLOAT){
    1111 			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
    1112 		}
    1113 	}
    1114
    1115 	/***
    1116 	 * Ensures the specific preconditions of the said instruction.
    1117 	 */
    1118 	public void visitFNEG(FNEG o){
    1119 		if (stack().peek() != Type.FLOAT){
    1120 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    1121 		}
    1122 	}
    1123
    1124 	/***
    1125 	 * Ensures the specific preconditions of the said instruction.
    1126 	 */
    1127 	public void visitFREM(FREM o){
    1128 		if (stack().peek() != Type.FLOAT){
    1129 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    1130 		}
    1131 		if (stack().peek(1) != Type.FLOAT){
    1132 			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
    1133 		}
    1134 	}
    1135
    1136 	/***
    1137 	 * Ensures the specific preconditions of the said instruction.
    1138 	 */
    1139 	public void visitFRETURN(FRETURN o){
    1140 		if (stack().peek() != Type.FLOAT){
    1141 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    1142 		}
    1143 	}
    1144
    1145 	/***
    1146 	 * Ensures the specific preconditions of the said instruction.
    1147 	 */
    1148 	public void visitFSTORE(FSTORE o){
    1149 		//visitStoreInstruction(StoreInstruction) is called before.
    1150
    1151 		// Nothing else needs to be done here.
    1152 	}
    1153
    1154 	/***
    1155 	 * Ensures the specific preconditions of the said instruction.
    1156 	 */
    1157 	public void visitFSUB(FSUB o){
    1158 		if (stack().peek() != Type.FLOAT){
    1159 			constraintViolated(o, "The value at the stack top is not of type 'float', but of type '"+stack().peek()+"'.");
    1160 		}
    1161 		if (stack().peek(1) != Type.FLOAT){
    1162 			constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '"+stack().peek(1)+"'.");
    1163 		}
    1164 	}
    1165
    1166 	/***
    1167 	 * Ensures the specific preconditions of the said instruction.
    1168 	 */
    1169 	public void visitGETFIELD(GETFIELD o){
    1170 		Type objectref = stack().peek();
    1171 		if (! ( (objectref instanceof ObjectType) || (objectref == Type.NULL) ) ){
    1172 			constraintViolated(o, "Stack top should be an object reference that's not an array reference, but is '"+objectref+"'.");
    1173 		}
    1174
    1175 		String field_name = o.getFieldName(cpg);
    1176
    1177 		JavaClass jc = Repository.lookupClass(o.getClassType(cpg).getClassName());
    1178 		Field[] fields = jc.getFields();
    1179 		Field f = null;
    1180 		for (int i=0; i<fields.length; i++){
    1181 			if (fields[i].getName().equals(field_name)){
    1182 				f = fields[i];
    1183 				break;
    1184 			}
    1185 		}
    1186 		if (f == null){
    1187 			throw new AssertionViolatedException("Field not found?!?");
    1188 		}
    1189
    1190 		if (f.isProtected()){
    1191 			ObjectType classtype = o.getClassType(cpg);
    1192 			ObjectType curr = new ObjectType(mg.getClassName());
    1193
    1194 			if (	classtype.equals(curr) ||
    1195 						curr.subclassOf(classtype)	){
    1196 				Type t = stack().peek();
    1197 				if (t == Type.NULL){
    1198 					return;
    1199 				}
    1200 				if (! (t instanceof ObjectType) ){
    1201 					constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '"+t+"'.");
    1202 				}
    1203 				ObjectType objreftype = (ObjectType) t;
    1204 				if (! ( objreftype.equals(curr) ||
    1205 						    objreftype.subclassOf(curr) ) ){
    1206 					//TODO: One day move to Staerk-et-al's "Set of object types" instead of "wider" object types
    1207 					//      created during the verification.
    1208 					//      "Wider" object types don't allow us to check for things like that below.
    1209 					//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.");
    1210 				}
    1211 			}
    1212 		}
    1213
    1214 		// TODO: Could go into Pass 3a.
    1215 		if (f.isStatic()){
    1216 			constraintViolated(o, "Referenced field '"+f+"' is static which it shouldn't be.");
    1217 		}
    1218 	}
    1219
    1220 	/***
    1221 	 * Ensures the specific preconditions of the said instruction.
    1222 	 */
    1223 	public void visitGETSTATIC(GETSTATIC o){
    1224 		// Field must be static: see Pass 3a.
    1225 	}
    1226
    1227 	/***
    1228 	 * Ensures the specific preconditions of the said instruction.
    1229 	 */
    1230 	public void visitGOTO(GOTO o){
    1231 		// nothing to do here.
    1232 	}
    1233
    1234 	/***
    1235 	 * Ensures the specific preconditions of the said instruction.
    1236 	 */
    1237 	public void visitGOTO_W(GOTO_W o){
    1238 		// nothing to do here.
    1239 	}
    1240
    1241 	/***
    1242 	 * Ensures the specific preconditions of the said instruction.
    1243 	 */
    1244 	public void visitI2B(I2B o){
    1245 		if (stack().peek() != Type.INT){
    1246 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1247 		}
    1248 	}
    1249
    1250 	/***
    1251 	 * Ensures the specific preconditions of the said instruction.
    1252 	 */
    1253 	public void visitI2C(I2C o){
    1254 		if (stack().peek() != Type.INT){
    1255 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1256 		}
    1257 	}
    1258
    1259 	/***
    1260 	 * Ensures the specific preconditions of the said instruction.
    1261 	 */
    1262 	public void visitI2D(I2D o){
    1263 		if (stack().peek() != Type.INT){
    1264 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1265 		}
    1266 	}
    1267
    1268 	/***
    1269 	 * Ensures the specific preconditions of the said instruction.
    1270 	 */
    1271 	public void visitI2F(I2F o){
    1272 		if (stack().peek() != Type.INT){
    1273 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1274 		}
    1275 	}
    1276
    1277 	/***
    1278 	 * Ensures the specific preconditions of the said instruction.
    1279 	 */
    1280 	public void visitI2L(I2L o){
    1281 		if (stack().peek() != Type.INT){
    1282 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1283 		}
    1284 	}
    1285
    1286 	/***
    1287 	 * Ensures the specific preconditions of the said instruction.
    1288 	 */
    1289 	public void visitI2S(I2S o){
    1290 		if (stack().peek() != Type.INT){
    1291 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1292 		}
    1293 	}
    1294
    1295 	/***
    1296 	 * Ensures the specific preconditions of the said instruction.
    1297 	 */
    1298 	public void visitIADD(IADD o){
    1299 		if (stack().peek() != Type.INT){
    1300 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1301 		}
    1302 		if (stack().peek(1) != Type.INT){
    1303 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1304 		}
    1305 	}
    1306
    1307 	/***
    1308 	 * Ensures the specific preconditions of the said instruction.
    1309 	 */
    1310 	public void visitIALOAD(IALOAD o){
    1311 		indexOfInt(o, stack().peek());
    1312 		if (stack().peek(1) == Type.NULL){
    1313 			return;
    1314 		}
    1315 		if (! (stack().peek(1) instanceof ArrayType)){
    1316 			constraintViolated(o, "Stack next-to-top must be of type int[] but is '"+stack().peek(1)+"'.");
    1317 		}
    1318 		Type t = ((ArrayType) (stack().peek(1))).getBasicType();
    1319 		if (t != Type.INT){
    1320 			constraintViolated(o, "Stack next-to-top must be of type int[] but is '"+stack().peek(1)+"'.");
    1321 		}
    1322 	}
    1323
    1324 	/***
    1325 	 * Ensures the specific preconditions of the said instruction.
    1326 	 */
    1327 	public void visitIAND(IAND o){
    1328 		if (stack().peek() != Type.INT){
    1329 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1330 		}
    1331 		if (stack().peek(1) != Type.INT){
    1332 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1333 		}
    1334 	}
    1335
    1336 	/***
    1337 	 * Ensures the specific preconditions of the said instruction.
    1338 	 */
    1339 	public void visitIASTORE(IASTORE o){
    1340 		if (stack().peek() != Type.INT){
    1341 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1342 		}
    1343 		indexOfInt(o, stack().peek(1));
    1344 		if (stack().peek(2) == Type.NULL){
    1345 			return;
    1346 		}
    1347 		if (! (stack().peek(2) instanceof ArrayType)){
    1348 			constraintViolated(o, "Stack next-to-next-to-top must be of type int[] but is '"+stack().peek(2)+"'.");
    1349 		}
    1350 		Type t = ((ArrayType) (stack().peek(2))).getBasicType();
    1351 		if (t != Type.INT){
    1352 			constraintViolated(o, "Stack next-to-next-to-top must be of type int[] but is '"+stack().peek(2)+"'.");
    1353 		}
    1354 	}
    1355
    1356 	/***
    1357 	 * Ensures the specific preconditions of the said instruction.
    1358 	 */
    1359 	public void visitICONST(ICONST o){
    1360 		//nothing to do here.
    1361 	}
    1362
    1363 	/***
    1364 	 * Ensures the specific preconditions of the said instruction.
    1365 	 */
    1366 	public void visitIDIV(IDIV o){
    1367 		if (stack().peek() != Type.INT){
    1368 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1369 		}
    1370 		if (stack().peek(1) != Type.INT){
    1371 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1372 		}
    1373 	}
    1374
    1375 	/***
    1376 	 * Ensures the specific preconditions of the said instruction.
    1377 	 */
    1378 	public void visitIF_ACMPEQ(IF_ACMPEQ o){
    1379 		if (!(stack().peek() instanceof ReferenceType)){
    1380 			constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '"+stack().peek()+"'.");
    1381 		}
    1382 		referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    1383
    1384 		if (!(stack().peek(1) instanceof ReferenceType)){
    1385 			constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '"+stack().peek(1)+"'.");
    1386 		}
    1387 		referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) );
    1388
    1389 	}
    1390
    1391 	/***
    1392 	 * Ensures the specific preconditions of the said instruction.
    1393 	 */
    1394 	public void visitIF_ACMPNE(IF_ACMPNE o){
    1395 		if (!(stack().peek() instanceof ReferenceType)){
    1396 			constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '"+stack().peek()+"'.");
    1397 			referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    1398 		}
    1399 		if (!(stack().peek(1) instanceof ReferenceType)){
    1400 			constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '"+stack().peek(1)+"'.");
    1401 			referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) );
    1402 		}
    1403 	}
    1404
    1405 	/***
    1406 	 * Ensures the specific preconditions of the said instruction.
    1407 	 */
    1408 	public void visitIF_ICMPEQ(IF_ICMPEQ o){
    1409 		if (stack().peek() != Type.INT){
    1410 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1411 		}
    1412 		if (stack().peek(1) != Type.INT){
    1413 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1414 		}
    1415 	}
    1416
    1417 	/***
    1418 	 * Ensures the specific preconditions of the said instruction.
    1419 	 */
    1420 	public void visitIF_ICMPGE(IF_ICMPGE o){
    1421 		if (stack().peek() != Type.INT){
    1422 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1423 		}
    1424 		if (stack().peek(1) != Type.INT){
    1425 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1426 		}
    1427 	}
    1428
    1429 	/***
    1430 	 * Ensures the specific preconditions of the said instruction.
    1431 	 */
    1432 	public void visitIF_ICMPGT(IF_ICMPGT o){
    1433 		if (stack().peek() != Type.INT){
    1434 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1435 		}
    1436 		if (stack().peek(1) != Type.INT){
    1437 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1438 		}
    1439 	}
    1440
    1441 	/***
    1442 	 * Ensures the specific preconditions of the said instruction.
    1443 	 */
    1444 	public void visitIF_ICMPLE(IF_ICMPLE o){
    1445 		if (stack().peek() != Type.INT){
    1446 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1447 		}
    1448 		if (stack().peek(1) != Type.INT){
    1449 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1450 		}
    1451 	}
    1452
    1453 	/***
    1454 	 * Ensures the specific preconditions of the said instruction.
    1455 	 */
    1456 	public void visitIF_ICMPLT(IF_ICMPLT o){
    1457 		if (stack().peek() != Type.INT){
    1458 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1459 		}
    1460 		if (stack().peek(1) != Type.INT){
    1461 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1462 		}
    1463 	}
    1464
    1465 	/***
    1466 	 * Ensures the specific preconditions of the said instruction.
    1467 	 */
    1468 	public void visitIF_ICMPNE(IF_ICMPNE o){
    1469 		if (stack().peek() != Type.INT){
    1470 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1471 		}
    1472 		if (stack().peek(1) != Type.INT){
    1473 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1474 		}
    1475 	}
    1476
    1477 	/***
    1478 	 * Ensures the specific preconditions of the said instruction.
    1479 	 */
    1480 	public void visitIFEQ(IFEQ o){
    1481 		if (stack().peek() != Type.INT){
    1482 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1483 		}
    1484 	}
    1485
    1486 	/***
    1487 	 * Ensures the specific preconditions of the said instruction.
    1488 	 */
    1489 	public void visitIFGE(IFGE o){
    1490 		if (stack().peek() != Type.INT){
    1491 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1492 		}
    1493 	}
    1494
    1495 	/***
    1496 	 * Ensures the specific preconditions of the said instruction.
    1497 	 */
    1498 	public void visitIFGT(IFGT o){
    1499 		if (stack().peek() != Type.INT){
    1500 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1501 		}
    1502 	}
    1503
    1504 	/***
    1505 	 * Ensures the specific preconditions of the said instruction.
    1506 	 */
    1507 	public void visitIFLE(IFLE o){
    1508 		if (stack().peek() != Type.INT){
    1509 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1510 		}
    1511 	}
    1512
    1513 	/***
    1514 	 * Ensures the specific preconditions of the said instruction.
    1515 	 */
    1516 	public void visitIFLT(IFLT o){
    1517 		if (stack().peek() != Type.INT){
    1518 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1519 		}
    1520 	}
    1521
    1522 	/***
    1523 	 * Ensures the specific preconditions of the said instruction.
    1524 	 */
    1525 	public void visitIFNE(IFNE o){
    1526 		if (stack().peek() != Type.INT){
    1527 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1528 		}
    1529 	}
    1530
    1531 	/***
    1532 	 * Ensures the specific preconditions of the said instruction.
    1533 	 */
    1534 	public void visitIFNONNULL(IFNONNULL o){
    1535 		if (!(stack().peek() instanceof ReferenceType)){
    1536 			constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '"+stack().peek()+"'.");
    1537 		}
    1538 		referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    1539 	}
    1540
    1541 	/***
    1542 	 * Ensures the specific preconditions of the said instruction.
    1543 	 */
    1544 	public void visitIFNULL(IFNULL o){
    1545 		if (!(stack().peek() instanceof ReferenceType)){
    1546 			constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '"+stack().peek()+"'.");
    1547 		}
    1548 		referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    1549 	}
    1550
    1551 	/***
    1552 	 * Ensures the specific preconditions of the said instruction.
    1553 	 */
    1554 	public void visitIINC(IINC o){
    1555 		// Mhhh. In BCEL, at this time "IINC" is not a LocalVariableInstruction.
    1556 		if (locals().maxLocals() <= (o.getType(cpg).getSize()==1? o.getIndex() : o.getIndex()+1) ){
    1557 			constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
    1558 		}
    1559
    1560 		indexOfInt(o, locals().get(o.getIndex()));
    1561 	}
    1562
    1563 	/***
    1564 	 * Ensures the specific preconditions of the said instruction.
    1565 	 */
    1566 	public void visitILOAD(ILOAD o){
    1567 		// All done by visitLocalVariableInstruction(), visitLoadInstruction()
    1568 	}
    1569
    1570 	/***
    1571 	 * Ensures the specific preconditions of the said instruction.
    1572 	 */
    1573 	public void visitIMPDEP1(IMPDEP1 o){
    1574 		throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP1.");
    1575 	}
    1576
    1577 	/***
    1578 	 * Ensures the specific preconditions of the said instruction.
    1579 	 */
    1580 	public void visitIMPDEP2(IMPDEP2 o){
    1581 		throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP2.");
    1582 	}
    1583
    1584 	/***
    1585 	 * Ensures the specific preconditions of the said instruction.
    1586 	 */
    1587 	public void visitIMUL(IMUL o){
    1588 		if (stack().peek() != Type.INT){
    1589 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1590 		}
    1591 		if (stack().peek(1) != Type.INT){
    1592 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1593 		}
    1594 	}
    1595
    1596 	/***
    1597 	 * Ensures the specific preconditions of the said instruction.
    1598 	 */
    1599 	public void visitINEG(INEG o){
    1600 		if (stack().peek() != Type.INT){
    1601 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1602 		}
    1603 	}
    1604
    1605 	/***
    1606 	 * Ensures the specific preconditions of the said instruction.
    1607 	 */
    1608 	public void visitINSTANCEOF(INSTANCEOF o){
    1609 		// The objectref must be of type reference.
    1610 		Type objectref = stack().peek(0);
    1611 		if (!(objectref instanceof ReferenceType)){
    1612 			constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type "+objectref+".");
    1613 		}
    1614 		else{
    1615 			referenceTypeIsInitialized(o, (ReferenceType) objectref);
    1616 		}
    1617 		// The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
    1618 		// current class (§3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
    1619 		// pool item at the index must be a symbolic reference to a class, array, or interface type.
    1620 		Constant c = cpg.getConstant(o.getIndex());
    1621 		if (! (c instanceof ConstantClass)){
    1622 			constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '"+c+"'.");
    1623 		}
    1624 	}
    1625
    1626 	/***
    1627 	 * Ensures the specific preconditions of the said instruction.
    1628 	 */
    1629 	public void visitINVOKEINTERFACE(INVOKEINTERFACE o){
    1630 		// Method is not native, otherwise pass 3 would not happen.
    1631
    1632 		int count = o.getCount();
    1633 		if (count == 0){
    1634 			constraintViolated(o, "The 'count' argument must not be 0.");
    1635 		}
    1636 		// It is a ConstantInterfaceMethodref, Pass 3a made it sure.
    1637 		// TODO: Do we want to do anything with it?
    1638         //ConstantInterfaceMethodref cimr = (ConstantInterfaceMethodref) (cpg.getConstant(o.getIndex()));
    1639
    1640 		// the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
    1641
    1642 		Type t = o.getType(cpg);
    1643 		if (t instanceof ObjectType){
    1644 			String name = ((ObjectType)t).getClassName();
    1645 			Verifier v = VerifierFactory.getVerifier( name );
    1646 			VerificationResult vr = v.doPass2();
    1647 			if (vr.getStatus() != VerificationResult.VERIFIED_OK){
    1648 				constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
    1649 			}
    1650 		}
    1651
    1652
    1653 		Type[] argtypes = o.getArgumentTypes(cpg);
    1654 		int nargs = argtypes.length;
    1655
    1656 		for (int i=nargs-1; i>=0; i--){
    1657 			Type fromStack = stack().peek( (nargs-1) - i );	// 0 to nargs-1
    1658 			Type fromDesc = argtypes[i];
    1659 			if (fromDesc == Type.BOOLEAN ||
    1660 					fromDesc == Type.BYTE ||
    1661 					fromDesc == Type.CHAR ||
    1662 					fromDesc == Type.SHORT){
    1663 				fromDesc = Type.INT;
    1664 			}
    1665 			if (! fromStack.equals(fromDesc)){
    1666 				if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType){
    1667 					//ReferenceType rFromStack = (ReferenceType) fromStack;
    1668 					//ReferenceType rFromDesc = (ReferenceType) fromDesc;
    1669 					// TODO: This can only be checked when using Staerk-et-al's "set of object types"
    1670 					// instead of a "wider cast object type" created during verification.
    1671 					//if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ){
    1672 					//	constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack (which is not assignment compatible).");
    1673 					//}
    1674 				}
    1675 				else{
    1676 					constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack.");
    1677 				}
    1678 			}
    1679 		}
    1680
    1681 		Type objref = stack().peek(nargs);
    1682 		if (objref == Type.NULL){
    1683 			return;
    1684 		}
    1685 		if (! (objref instanceof ReferenceType) ){
    1686 			constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '"+objref+"'.");
    1687 		}
    1688 		referenceTypeIsInitialized(o, (ReferenceType) objref);
    1689 		if (!(objref instanceof ObjectType)){
    1690 			if (!(objref instanceof ArrayType)){
    1691 				constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '"+objref+"'."); // could be a ReturnaddressType
    1692 			}
    1693 			else{
    1694 				objref = GENERIC_ARRAY;
    1695 			}
    1696 		}
    1697
    1698 		// String objref_classname = ((ObjectType) objref).getClassName();
    1699 	    // String theInterface = o.getClassName(cpg);
    1700 		// TODO: This can only be checked if we're using Staerk-et-al's "set of object types"
    1701 		//       instead of "wider cast object types" generated during verification.
    1702 		//if ( ! Repository.implementationOf(objref_classname, theInterface) ){
    1703 		//	constraintViolated(o, "The 'objref' item '"+objref+"' does not implement '"+theInterface+"' as expected.");
    1704 		//}
    1705
    1706 		int counted_count = 1; // 1 for the objectref
    1707 		for (int i=0; i<nargs; i++){
    1708 			counted_count += argtypes[i].getSize();
    1709 		}
    1710 		if (count != counted_count){
    1711 			constraintViolated(o, "The 'count' argument should probably read '"+counted_count+"' but is '"+count+"'.");
    1712 		}
    1713 	}
    1714
    1715 	/***
    1716 	 * Ensures the specific preconditions of the said instruction.
    1717 	 */
    1718 	public void visitINVOKESPECIAL(INVOKESPECIAL o){
    1719 		// Don't init an object twice.
    1720 		if ( (o.getMethodName(cpg).equals(Constants.CONSTRUCTOR_NAME)) && (!(stack().peek(o.getArgumentTypes(cpg).length) instanceof UninitializedObjectType)) ){
    1721 			constraintViolated(o, "Possibly initializing object twice. A valid instruction sequence must not have an uninitialized object on the operand stack or in a local variable during a backwards branch, or in a local variable in code protected by an exception handler. Please see The Java Virtual Machine Specification, Second Edition, 4.9.4 (pages 147 and 148) for details.");
    1722 		}
    1723
    1724 		// the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
    1725
    1726 		Type t = o.getType(cpg);
    1727 		if (t instanceof ObjectType){
    1728 			String name = ((ObjectType)t).getClassName();
    1729 			Verifier v = VerifierFactory.getVerifier( name );
    1730 			VerificationResult vr = v.doPass2();
    1731 			if (vr.getStatus() != VerificationResult.VERIFIED_OK){
    1732 				constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
    1733 			}
    1734 		}
    1735
    1736
    1737 		Type[] argtypes = o.getArgumentTypes(cpg);
    1738 		int nargs = argtypes.length;
    1739
    1740 		for (int i=nargs-1; i>=0; i--){
    1741 			Type fromStack = stack().peek( (nargs-1) - i );	// 0 to nargs-1
    1742 			Type fromDesc = argtypes[i];
    1743 			if (fromDesc == Type.BOOLEAN ||
    1744 					fromDesc == Type.BYTE ||
    1745 					fromDesc == Type.CHAR ||
    1746 					fromDesc == Type.SHORT){
    1747 				fromDesc = Type.INT;
    1748 			}
    1749 			if (! fromStack.equals(fromDesc)){
    1750 				if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType){
    1751 					ReferenceType rFromStack = (ReferenceType) fromStack;
    1752 					ReferenceType rFromDesc = (ReferenceType) fromDesc;
    1753 					// TODO: This can only be checked using Staerk-et-al's "set of object types", not
    1754 					// using a "wider cast object type".
    1755 					if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ){
    1756 						constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack (which is not assignment compatible).");
    1757 					}
    1758 				}
    1759 				else{
    1760 					constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack.");
    1761 				}
    1762 			}
    1763 		}
    1764
    1765 		Type objref = stack().peek(nargs);
    1766 		if (objref == Type.NULL){
    1767 			return;
    1768 		}
    1769 		if (! (objref instanceof ReferenceType) ){
    1770 			constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '"+objref+"'.");
    1771 		}
    1772 		String objref_classname = null;
    1773 		if ( !(o.getMethodName(cpg).equals(Constants.CONSTRUCTOR_NAME))){
    1774 			referenceTypeIsInitialized(o, (ReferenceType) objref);
    1775 			if (!(objref instanceof ObjectType)){
    1776 				if (!(objref instanceof ArrayType)){
    1777 					constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '"+objref+"'."); // could be a ReturnaddressType
    1778 				}
    1779 				else{
    1780 					objref = GENERIC_ARRAY;
    1781 				}
    1782 			}
    1783
    1784 			objref_classname = ((ObjectType) objref).getClassName();
    1785 		}
    1786 		else{
    1787 			if (!(objref instanceof UninitializedObjectType)){
    1788 				constraintViolated(o, "Expecting an UninitializedObjectType as 'objectref' on the stack, not a '"+objref+"'. Otherwise, you couldn't invoke a method since an array has no methods (not to speak of a return address).");
    1789 			}
    1790 			objref_classname = ((UninitializedObjectType) objref).getInitialized().getClassName();
    1791 		}
    1792
    1793
    1794 		String theClass = o.getClassName(cpg);
    1795 		if ( ! Repository.instanceOf(objref_classname, theClass) ){
    1796 			constraintViolated(o, "The 'objref' item '"+objref+"' does not implement '"+theClass+"' as expected.");
    1797 		}
    1798
    1799 	}
    1800
    1801 	/***
    1802 	 * Ensures the specific preconditions of the said instruction.
    1803 	 */
    1804 	public void visitINVOKESTATIC(INVOKESTATIC o){
    1805 		// Method is not native, otherwise pass 3 would not happen.
    1806
    1807 		Type t = o.getType(cpg);
    1808 		if (t instanceof ObjectType){
    1809 			String name = ((ObjectType)t).getClassName();
    1810 			Verifier v = VerifierFactory.getVerifier( name );
    1811 			VerificationResult vr = v.doPass2();
    1812 			if (vr.getStatus() != VerificationResult.VERIFIED_OK){
    1813 				constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
    1814 			}
    1815 		}
    1816
    1817 		Type[] argtypes = o.getArgumentTypes(cpg);
    1818 		int nargs = argtypes.length;
    1819
    1820 		for (int i=nargs-1; i>=0; i--){
    1821 			Type fromStack = stack().peek( (nargs-1) - i );	// 0 to nargs-1
    1822 			Type fromDesc = argtypes[i];
    1823 			if (fromDesc == Type.BOOLEAN ||
    1824 					fromDesc == Type.BYTE ||
    1825 					fromDesc == Type.CHAR ||
    1826 					fromDesc == Type.SHORT){
    1827 				fromDesc = Type.INT;
    1828 			}
    1829 			if (! fromStack.equals(fromDesc)){
    1830 				if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType){
    1831 					ReferenceType rFromStack = (ReferenceType) fromStack;
    1832 					ReferenceType rFromDesc = (ReferenceType) fromDesc;
    1833 					// TODO: This check can possibly only be done using Staerk-et-al's "set of object types"
    1834 					// instead of a "wider cast object type" created during verification.
    1835 					if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ){
    1836 						constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack (which is not assignment compatible).");
    1837 					}
    1838 				}
    1839 				else{
    1840 					constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack.");
    1841 				}
    1842 			}
    1843 		}
    1844 	}
    1845
    1846 	/***
    1847 	 * Ensures the specific preconditions of the said instruction.
    1848 	 */
    1849 	public void visitINVOKEVIRTUAL(INVOKEVIRTUAL o){
    1850 		// the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
    1851
    1852 		Type t = o.getType(cpg);
    1853 		if (t instanceof ObjectType){
    1854 			String name = ((ObjectType)t).getClassName();
    1855 			Verifier v = VerifierFactory.getVerifier( name );
    1856 			VerificationResult vr = v.doPass2();
    1857 			if (vr.getStatus() != VerificationResult.VERIFIED_OK){
    1858 				constraintViolated((Instruction) o, "Class '"+name+"' is referenced, but cannot be loaded and resolved: '"+vr+"'.");
    1859 			}
    1860 		}
    1861
    1862
    1863 		Type[] argtypes = o.getArgumentTypes(cpg);
    1864 		int nargs = argtypes.length;
    1865
    1866 		for (int i=nargs-1; i>=0; i--){
    1867 			Type fromStack = stack().peek( (nargs-1) - i );	// 0 to nargs-1
    1868 			Type fromDesc = argtypes[i];
    1869 			if (fromDesc == Type.BOOLEAN ||
    1870 					fromDesc == Type.BYTE ||
    1871 					fromDesc == Type.CHAR ||
    1872 					fromDesc == Type.SHORT){
    1873 				fromDesc = Type.INT;
    1874 			}
    1875 			if (! fromStack.equals(fromDesc)){
    1876 				if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType){
    1877 					ReferenceType rFromStack = (ReferenceType) fromStack;
    1878 					ReferenceType rFromDesc = (ReferenceType) fromDesc;
    1879 					// TODO: This can possibly only be checked when using Staerk-et-al's "set of object types" instead
    1880 					// of a single "wider cast object type" created during verification.
    1881 					if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ){
    1882 						constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack (which is not assignment compatible).");
    1883 					}
    1884 				}
    1885 				else{
    1886 					constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+"' on the stack.");
    1887 				}
    1888 			}
    1889 		}
    1890
    1891 		Type objref = stack().peek(nargs);
    1892 		if (objref == Type.NULL){
    1893 			return;
    1894 		}
    1895 		if (! (objref instanceof ReferenceType) ){
    1896 			constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '"+objref+"'.");
    1897 		}
    1898 		referenceTypeIsInitialized(o, (ReferenceType) objref);
    1899 		if (!(objref instanceof ObjectType)){
    1900 			if (!(objref instanceof ArrayType)){
    1901 				constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '"+objref+"'."); // could be a ReturnaddressType
    1902 			}
    1903 			else{
    1904 				objref = GENERIC_ARRAY;
    1905 			}
    1906 		}
    1907
    1908 		String objref_classname = ((ObjectType) objref).getClassName();
    1909
    1910 		String theClass = o.getClassName(cpg);
    1911
    1912 		if ( ! Repository.instanceOf(objref_classname, theClass) ){
    1913 			constraintViolated(o, "The 'objref' item '"+objref+"' does not implement '"+theClass+"' as expected.");
    1914 		}
    1915 	}
    1916
    1917 	/***
    1918 	 * Ensures the specific preconditions of the said instruction.
    1919 	 */
    1920 	public void visitIOR(IOR o){
    1921 		if (stack().peek() != Type.INT){
    1922 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1923 		}
    1924 		if (stack().peek(1) != Type.INT){
    1925 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1926 		}
    1927 	}
    1928
    1929 	/***
    1930 	 * Ensures the specific preconditions of the said instruction.
    1931 	 */
    1932 	public void visitIREM(IREM o){
    1933 		if (stack().peek() != Type.INT){
    1934 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1935 		}
    1936 		if (stack().peek(1) != Type.INT){
    1937 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1938 		}
    1939 	}
    1940
    1941 	/***
    1942 	 * Ensures the specific preconditions of the said instruction.
    1943 	 */
    1944 	public void visitIRETURN(IRETURN o){
    1945 		if (stack().peek() != Type.INT){
    1946 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1947 		}
    1948 	}
    1949
    1950 	/***
    1951 	 * Ensures the specific preconditions of the said instruction.
    1952 	 */
    1953 	public void visitISHL(ISHL o){
    1954 		if (stack().peek() != Type.INT){
    1955 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1956 		}
    1957 		if (stack().peek(1) != Type.INT){
    1958 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1959 		}
    1960 	}
    1961
    1962 	/***
    1963 	 * Ensures the specific preconditions of the said instruction.
    1964 	 */
    1965 	public void visitISHR(ISHR o){
    1966 		if (stack().peek() != Type.INT){
    1967 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1968 		}
    1969 		if (stack().peek(1) != Type.INT){
    1970 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1971 		}
    1972 	}
    1973
    1974 	/***
    1975 	 * Ensures the specific preconditions of the said instruction.
    1976 	 */
    1977 	public void visitISTORE(ISTORE o){
    1978 		//visitStoreInstruction(StoreInstruction) is called before.
    1979
    1980 		// Nothing else needs to be done here.
    1981 	}
    1982
    1983 	/***
    1984 	 * Ensures the specific preconditions of the said instruction.
    1985 	 */
    1986 	public void visitISUB(ISUB o){
    1987 		if (stack().peek() != Type.INT){
    1988 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    1989 		}
    1990 		if (stack().peek(1) != Type.INT){
    1991 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    1992 		}
    1993 	}
    1994
    1995 	/***
    1996 	 * Ensures the specific preconditions of the said instruction.
    1997 	 */
    1998 	public void visitIUSHR(IUSHR o){
    1999 		if (stack().peek() != Type.INT){
    2000 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    2001 		}
    2002 		if (stack().peek(1) != Type.INT){
    2003 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    2004 		}
    2005 	}
    2006
    2007 	/***
    2008 	 * Ensures the specific preconditions of the said instruction.
    2009 	 */
    2010 	public void visitIXOR(IXOR o){
    2011 		if (stack().peek() != Type.INT){
    2012 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    2013 		}
    2014 		if (stack().peek(1) != Type.INT){
    2015 			constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '"+stack().peek(1)+"'.");
    2016 		}
    2017 	}
    2018
    2019 	/***
    2020 	 * Ensures the specific preconditions of the said instruction.
    2021 	 */
    2022 	public void visitJSR(JSR o){
    2023 		// nothing to do here.
    2024 	}
    2025
    2026 	/***
    2027 	 * Ensures the specific preconditions of the said instruction.
    2028 	 */
    2029 	public void visitJSR_W(JSR_W o){
    2030 		// nothing to do here.
    2031 	}
    2032
    2033 	/***
    2034 	 * Ensures the specific preconditions of the said instruction.
    2035 	 */
    2036 	public void visitL2D(L2D o){
    2037 		if (stack().peek() != Type.LONG){
    2038 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2039 		}
    2040 	}
    2041
    2042 	/***
    2043 	 * Ensures the specific preconditions of the said instruction.
    2044 	 */
    2045 	public void visitL2F(L2F o){
    2046 		if (stack().peek() != Type.LONG){
    2047 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2048 		}
    2049 	}
    2050
    2051 	/***
    2052 	 * Ensures the specific preconditions of the said instruction.
    2053 	 */
    2054 	public void visitL2I(L2I o){
    2055 		if (stack().peek() != Type.LONG){
    2056 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2057 		}
    2058 	}
    2059
    2060 	/***
    2061 	 * Ensures the specific preconditions of the said instruction.
    2062 	 */
    2063 	public void visitLADD(LADD o){
    2064 		if (stack().peek() != Type.LONG){
    2065 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2066 		}
    2067 		if (stack().peek(1) != Type.LONG){
    2068 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2069 		}
    2070 	}
    2071
    2072 	/***
    2073 	 * Ensures the specific preconditions of the said instruction.
    2074 	 */
    2075 	public void visitLALOAD(LALOAD o){
    2076 		indexOfInt(o, stack().peek());
    2077 		if (stack().peek(1) == Type.NULL){
    2078 			return;
    2079 		}
    2080 		if (! (stack().peek(1) instanceof ArrayType)){
    2081 			constraintViolated(o, "Stack next-to-top must be of type long[] but is '"+stack().peek(1)+"'.");
    2082 		}
    2083 		Type t = ((ArrayType) (stack().peek(1))).getBasicType();
    2084 		if (t != Type.LONG){
    2085 			constraintViolated(o, "Stack next-to-top must be of type long[] but is '"+stack().peek(1)+"'.");
    2086 		}
    2087 	}
    2088
    2089 	/***
    2090 	 * Ensures the specific preconditions of the said instruction.
    2091 	 */
    2092 	public void visitLAND(LAND o){
    2093 		if (stack().peek() != Type.LONG){
    2094 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2095 		}
    2096 		if (stack().peek(1) != Type.LONG){
    2097 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2098 		}
    2099 	}
    2100
    2101 	/***
    2102 	 * Ensures the specific preconditions of the said instruction.
    2103 	 */
    2104 	public void visitLASTORE(LASTORE o){
    2105 		if (stack().peek() != Type.LONG){
    2106 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2107 		}
    2108 		indexOfInt(o, stack().peek(1));
    2109 		if (stack().peek(2) == Type.NULL){
    2110 			return;
    2111 		}
    2112 		if (! (stack().peek(2) instanceof ArrayType)){
    2113 			constraintViolated(o, "Stack next-to-next-to-top must be of type long[] but is '"+stack().peek(2)+"'.");
    2114 		}
    2115 		Type t = ((ArrayType) (stack().peek(2))).getBasicType();
    2116 		if (t != Type.LONG){
    2117 			constraintViolated(o, "Stack next-to-next-to-top must be of type long[] but is '"+stack().peek(2)+"'.");
    2118 		}
    2119 	}
    2120
    2121 	/***
    2122 	 * Ensures the specific preconditions of the said instruction.
    2123 	 */
    2124 	public void visitLCMP(LCMP o){
    2125 		if (stack().peek() != Type.LONG){
    2126 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2127 		}
    2128 		if (stack().peek(1) != Type.LONG){
    2129 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2130 		}
    2131 	}
    2132
    2133 	/***
    2134 	 * Ensures the specific preconditions of the said instruction.
    2135 	 */
    2136 	public void visitLCONST(LCONST o){
    2137 		// Nothing to do here.
    2138 	}
    2139
    2140 	/***
    2141 	 * Ensures the specific preconditions of the said instruction.
    2142 	 */
    2143 	public void visitLDC(LDC o){
    2144 		// visitCPInstruction is called first.
    2145
    2146 		Constant c = cpg.getConstant(o.getIndex());
    2147 		if 	(!	(	( c instanceof ConstantInteger) ||
    2148 							( c instanceof ConstantFloat	)	||
    2149 							( c instanceof ConstantString )	)	){
    2150 			constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '"+c+"'.");
    2151 		}
    2152 	}
    2153
    2154 	/***
    2155 	 * Ensures the specific preconditions of the said instruction.
    2156 	 */
    2157 	public void visitLDC_W(LDC_W o){
    2158 		// visitCPInstruction is called first.
    2159
    2160 		Constant c = cpg.getConstant(o.getIndex());
    2161 		if 	(!	(	( c instanceof ConstantInteger) ||
    2162 							( c instanceof ConstantFloat	)	||
    2163 							( c instanceof ConstantString )	)	){
    2164 			constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '"+c+"'.");
    2165 		}
    2166 	}
    2167
    2168 	/***
    2169 	 * Ensures the specific preconditions of the said instruction.
    2170 	 */
    2171 	public void visitLDC2_W(LDC2_W o){
    2172 		// visitCPInstruction is called first.
    2173
    2174 		Constant c = cpg.getConstant(o.getIndex());
    2175 		if 	(!	(	( c instanceof ConstantLong) ||
    2176 							( c instanceof ConstantDouble )	)	){
    2177 			constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '"+c+"'.");
    2178 		}
    2179 	}
    2180
    2181 	/***
    2182 	 * Ensures the specific preconditions of the said instruction.
    2183 	 */
    2184 	public void visitLDIV(LDIV o){
    2185 		if (stack().peek() != Type.LONG){
    2186 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2187 		}
    2188 		if (stack().peek(1) != Type.LONG){
    2189 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2190 		}
    2191 	}
    2192
    2193 	/***
    2194 	 * Ensures the specific preconditions of the said instruction.
    2195 	 */
    2196 	public void visitLLOAD(LLOAD o){
    2197 		//visitLoadInstruction(LoadInstruction) is called before.
    2198
    2199 		// Nothing else needs to be done here.
    2200 	}
    2201
    2202 	/***
    2203 	 * Ensures the specific preconditions of the said instruction.
    2204 	 */
    2205 	public void visitLMUL(LMUL o){
    2206 		if (stack().peek() != Type.LONG){
    2207 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2208 		}
    2209 		if (stack().peek(1) != Type.LONG){
    2210 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2211 		}
    2212 	}
    2213
    2214 	/***
    2215 	 * Ensures the specific preconditions of the said instruction.
    2216 	 */
    2217 	public void visitLNEG(LNEG o){
    2218 		if (stack().peek() != Type.LONG){
    2219 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2220 		}
    2221 	}
    2222
    2223 	/***
    2224 	 * Ensures the specific preconditions of the said instruction.
    2225 	 */
    2226 	public void visitLOOKUPSWITCH(LOOKUPSWITCH o){
    2227 		if (stack().peek() != Type.INT){
    2228 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    2229 		}
    2230 		// See also pass 3a.
    2231 	}
    2232
    2233 	/***
    2234 	 * Ensures the specific preconditions of the said instruction.
    2235 	 */
    2236 	public void visitLOR(LOR o){
    2237 		if (stack().peek() != Type.LONG){
    2238 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2239 		}
    2240 		if (stack().peek(1) != Type.LONG){
    2241 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2242 		}
    2243 	}
    2244
    2245 	/***
    2246 	 * Ensures the specific preconditions of the said instruction.
    2247 	 */
    2248 	public void visitLREM(LREM o){
    2249 		if (stack().peek() != Type.LONG){
    2250 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2251 		}
    2252 		if (stack().peek(1) != Type.LONG){
    2253 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2254 		}
    2255 	}
    2256
    2257 	/***
    2258 	 * Ensures the specific preconditions of the said instruction.
    2259 	 */
    2260 	public void visitLRETURN(LRETURN o){
    2261 		if (stack().peek() != Type.LONG){
    2262 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2263 		}
    2264 	}
    2265
    2266 	/***
    2267 	 * Ensures the specific preconditions of the said instruction.
    2268 	 */
    2269 	public void visitLSHL(LSHL o){
    2270 		if (stack().peek() != Type.INT){
    2271 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    2272 		}
    2273 		if (stack().peek(1) != Type.LONG){
    2274 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2275 		}
    2276 	}
    2277
    2278 	/***
    2279 	 * Ensures the specific preconditions of the said instruction.
    2280 	 */
    2281 	public void visitLSHR(LSHR o){
    2282 		if (stack().peek() != Type.INT){
    2283 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    2284 		}
    2285 		if (stack().peek(1) != Type.LONG){
    2286 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2287 		}
    2288 	}
    2289
    2290 	/***
    2291 	 * Ensures the specific preconditions of the said instruction.
    2292 	 */
    2293 	public void visitLSTORE(LSTORE o){
    2294 		//visitStoreInstruction(StoreInstruction) is called before.
    2295
    2296 		// Nothing else needs to be done here.
    2297 	}
    2298
    2299 	/***
    2300 	 * Ensures the specific preconditions of the said instruction.
    2301 	 */
    2302 	public void visitLSUB(LSUB o){
    2303 		if (stack().peek() != Type.LONG){
    2304 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2305 		}
    2306 		if (stack().peek(1) != Type.LONG){
    2307 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2308 		}
    2309 	}
    2310
    2311 	/***
    2312 	 * Ensures the specific preconditions of the said instruction.
    2313 	 */
    2314 	public void visitLUSHR(LUSHR o){
    2315 		if (stack().peek() != Type.INT){
    2316 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    2317 		}
    2318 		if (stack().peek(1) != Type.LONG){
    2319 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2320 		}
    2321 	}
    2322
    2323 	/***
    2324 	 * Ensures the specific preconditions of the said instruction.
    2325 	 */
    2326 	public void visitLXOR(LXOR o){
    2327 		if (stack().peek() != Type.LONG){
    2328 			constraintViolated(o, "The value at the stack top is not of type 'long', but of type '"+stack().peek()+"'.");
    2329 		}
    2330 		if (stack().peek(1) != Type.LONG){
    2331 			constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '"+stack().peek(1)+"'.");
    2332 		}
    2333 	}
    2334
    2335 	/***
    2336 	 * Ensures the specific preconditions of the said instruction.
    2337 	 */
    2338 	public void visitMONITORENTER(MONITORENTER o){
    2339 		if (! ((stack().peek()) instanceof ReferenceType)){
    2340 			constraintViolated(o, "The stack top should be of a ReferenceType, but is '"+stack().peek()+"'.");
    2341 		}
    2342 		referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    2343 	}
    2344
    2345 	/***
    2346 	 * Ensures the specific preconditions of the said instruction.
    2347 	 */
    2348 	public void visitMONITOREXIT(MONITOREXIT o){
    2349 		if (! ((stack().peek()) instanceof ReferenceType)){
    2350 			constraintViolated(o, "The stack top should be of a ReferenceType, but is '"+stack().peek()+"'.");
    2351 		}
    2352 		referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    2353 	}
    2354
    2355 	/***
    2356 	 * Ensures the specific preconditions of the said instruction.
    2357 	 */
    2358 	public void visitMULTIANEWARRAY(MULTIANEWARRAY o){
    2359 		int dimensions = o.getDimensions();
    2360 		// Dimensions argument is okay: see Pass 3a.
    2361 		for (int i=0; i<dimensions; i++){
    2362 			if (stack().peek(i) != Type.INT){
    2363 				constraintViolated(o, "The '"+dimensions+"' upper stack types should be 'int' but aren't.");
    2364 			}
    2365 		}
    2366 		// The runtime constant pool item at that index must be a symbolic reference to a class,
    2367 		// array, or interface type. See Pass 3a.
    2368 	}
    2369
    2370 	/***
    2371 	 * Ensures the specific preconditions of the said instruction.
    2372 	 */
    2373 	public void visitNEW(NEW o){
    2374 		//visitCPInstruction(CPInstruction) has been called before.
    2375 		//visitLoadClass(LoadClass) has been called before.
    2376
    2377 		Type t = o.getType(cpg);
    2378 		if (! (t instanceof ReferenceType)){
    2379 			throw new AssertionViolatedException("NEW.getType() returning a non-reference type?!");
    2380 		}
    2381 		if (! (t instanceof ObjectType)){
    2382 			constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '"+t+"'.");
    2383 		}
    2384 		ObjectType obj = (ObjectType) t;
    2385
    2386 		//e.g.: Don't instantiate interfaces
    2387 		if (! obj.referencesClass()){
    2388 			constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '"+obj+"'.");
    2389 		}
    2390 	}
    2391
    2392 	/***
    2393 	 * Ensures the specific preconditions of the said instruction.
    2394 	 */
    2395 	public void visitNEWARRAY(NEWARRAY o){
    2396 		if (stack().peek() != Type.INT){
    2397 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    2398 		}
    2399 	}
    2400
    2401 	/***
    2402 	 * Ensures the specific preconditions of the said instruction.
    2403 	 */
    2404 	public void visitNOP(NOP o){
    2405 		// nothing is to be done here.
    2406 	}
    2407
    2408 	/***
    2409 	 * Ensures the specific preconditions of the said instruction.
    2410 	 */
    2411 	public void visitPOP(POP o){
    2412 		if (stack().peek().getSize() != 1){
    2413 			constraintViolated(o, "Stack top size should be 1 but stack top is '"+stack().peek()+"' of size '"+stack().peek().getSize()+"'.");
    2414 		}
    2415 	}
    2416
    2417 	/***
    2418 	 * Ensures the specific preconditions of the said instruction.
    2419 	 */
    2420 	public void visitPOP2(POP2 o){
    2421 		if (stack().peek().getSize() != 2){
    2422 			constraintViolated(o, "Stack top size should be 2 but stack top is '"+stack().peek()+"' of size '"+stack().peek().getSize()+"'.");
    2423 		}
    2424 	}
    2425
    2426 	/***
    2427 	 * Ensures the specific preconditions of the said instruction.
    2428 	 */
    2429 	public void visitPUTFIELD(PUTFIELD o){
    2430
    2431 		Type objectref = stack().peek(1);
    2432 		if (! ( (objectref instanceof ObjectType) || (objectref == Type.NULL) ) ){
    2433 			constraintViolated(o, "Stack next-to-top should be an object reference that's not an array reference, but is '"+objectref+"'.");
    2434 		}
    2435
    2436 		String field_name = o.getFieldName(cpg);
    2437
    2438 		JavaClass jc = Repository.lookupClass(o.getClassType(cpg).getClassName());
    2439 		Field[] fields = jc.getFields();
    2440 		Field f = null;
    2441 		for (int i=0; i<fields.length; i++){
    2442 			if (fields[i].getName().equals(field_name)){
    2443 				f = fields[i];
    2444 				break;
    2445 			}
    2446 		}
    2447 		if (f == null){
    2448 			throw new AssertionViolatedException("Field not found?!?");
    2449 		}
    2450
    2451 		Type value = stack().peek();
    2452 		Type t = Type.getType(f.getSignature());
    2453 		Type shouldbe = t;
    2454 		if (shouldbe == Type.BOOLEAN ||
    2455 				shouldbe == Type.BYTE ||
    2456 				shouldbe == Type.CHAR ||
    2457 				shouldbe == Type.SHORT){
    2458 			shouldbe = Type.INT;
    2459 		}
    2460 		if (t instanceof ReferenceType){
    2461 			ReferenceType rvalue = null;
    2462 			if (value instanceof ReferenceType){
    2463 				rvalue = (ReferenceType) value;
    2464 				referenceTypeIsInitialized(o, rvalue);
    2465 			}
    2466 			else{
    2467 				constraintViolated(o, "The stack top type '"+value+"' is not of a reference type as expected.");
    2468 			}
    2469 			// TODO: This can possibly only be checked using Staerk-et-al's "set-of-object types", not
    2470 			// using "wider cast object types" created during verification.
    2471 			// Comment it out if you encounter problems. See also the analogon at visitPUTSTATIC.
    2472 			if (!(rvalue.isAssignmentCompatibleWith(shouldbe))){
    2473 				constraintViolated(o, "The stack top type '"+value+"' is not assignment compatible with '"+shouldbe+"'.");
    2474 			}
    2475 		}
    2476 		else{
    2477 			if (shouldbe != value){
    2478 				constraintViolated(o, "The stack top type '"+value+"' is not of type '"+shouldbe+"' as expected.");
    2479 			}
    2480 		}
    2481
    2482 		if (f.isProtected()){
    2483 			ObjectType classtype = o.getClassType(cpg);
    2484 			ObjectType curr = new ObjectType(mg.getClassName());
    2485
    2486 			if (	classtype.equals(curr) ||
    2487 						curr.subclassOf(classtype)	){
    2488 				Type tp = stack().peek(1);
    2489 				if (tp == Type.NULL){
    2490 					return;
    2491 				}
    2492 				if (! (tp instanceof ObjectType) ){
    2493 					constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '"+tp+"'.");
    2494 				}
    2495 				ObjectType objreftype = (ObjectType) tp;
    2496 				if (! ( objreftype.equals(curr) ||
    2497 						    objreftype.subclassOf(curr) ) ){
    2498 					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.");
    2499 				}
    2500 			}
    2501 		}
    2502
    2503 		// TODO: Could go into Pass 3a.
    2504 		if (f.isStatic()){
    2505 			constraintViolated(o, "Referenced field '"+f+"' is static which it shouldn't be.");
    2506 		}
    2507 	}
    2508
    2509 	/***
    2510 	 * Ensures the specific preconditions of the said instruction.
    2511 	 */
    2512 	public void visitPUTSTATIC(PUTSTATIC o){
    2513 		String field_name = o.getFieldName(cpg);
    2514 		JavaClass jc = Repository.lookupClass(o.getClassType(cpg).getClassName());
    2515 		Field[] fields = jc.getFields();
    2516 		Field f = null;
    2517 		for (int i=0; i<fields.length; i++){
    2518 			if (fields[i].getName().equals(field_name)){
    2519 				f = fields[i];
    2520 				break;
    2521 			}
    2522 		}
    2523 		if (f == null){
    2524 			throw new AssertionViolatedException("Field not found?!?");
    2525 		}
    2526 		Type value = stack().peek();
    2527 		Type t = Type.getType(f.getSignature());
    2528 		Type shouldbe = t;
    2529 		if (shouldbe == Type.BOOLEAN ||
    2530 				shouldbe == Type.BYTE ||
    2531 				shouldbe == Type.CHAR ||
    2532 				shouldbe == Type.SHORT){
    2533 			shouldbe = Type.INT;
    2534 		}
    2535 		if (t instanceof ReferenceType){
    2536 			ReferenceType rvalue = null;
    2537 			if (value instanceof ReferenceType){
    2538 				rvalue = (ReferenceType) value;
    2539 				referenceTypeIsInitialized(o, rvalue);
    2540 			}
    2541 			else{
    2542 				constraintViolated(o, "The stack top type '"+value+"' is not of a reference type as expected.");
    2543 			}
    2544 			// TODO: This can possibly only be checked using Staerk-et-al's "set-of-object types", not
    2545 			// using "wider cast object types" created during verification.
    2546 			// Comment it out if you encounter problems. See also the analogon at visitPUTFIELD.
    2547 			if (!(rvalue.isAssignmentCompatibleWith(shouldbe))){
    2548 				constraintViolated(o, "The stack top type '"+value+"' is not assignment compatible with '"+shouldbe+"'.");
    2549 			}
    2550 		}
    2551 		else{
    2552 			if (shouldbe != value){
    2553 				constraintViolated(o, "The stack top type '"+value+"' is not of type '"+shouldbe+"' as expected.");
    2554 			}
    2555 		}
    2556 		// TODO: Interface fields may be assigned to only once. (Hard to implement in
    2557 		//       JustIce's execution model). This may only happen in <clinit>, see Pass 3a.
    2558 	}
    2559
    2560 	/***
    2561 	 * Ensures the specific preconditions of the said instruction.
    2562 	 */
    2563 	public void visitRET(RET o){
    2564 		if (! (locals().get(o.getIndex()) instanceof ReturnaddressType)){
    2565 			constraintViolated(o, "Expecting a ReturnaddressType in local variable "+o.getIndex()+".");
    2566 		}
    2567 		if (locals().get(o.getIndex()) == ReturnaddressType.NO_TARGET){
    2568 			throw new AssertionViolatedException("Oops: RET expecting a target!");
    2569 		}
    2570 		// Other constraints such as non-allowed overlapping subroutines are enforced
    2571 		// while building the Subroutines data structure.
    2572 	}
    2573
    2574 	/***
    2575 	 * Ensures the specific preconditions of the said instruction.
    2576 	 */
    2577 	public void visitRETURN(RETURN o){
    2578 		if (mg.getName().equals(Constants.CONSTRUCTOR_NAME)){// If we leave an <init> method
    2579 			if ((frame._this != null) && (!(mg.getClassName().equals(Type.OBJECT.getClassName()))) ) {
    2580 				constraintViolated(o, "Leaving a constructor that itself did not call a constructor.");
    2581 			}
    2582 		}
    2583 	}
    2584
    2585 	/***
    2586 	 * Ensures the specific preconditions of the said instruction.
    2587 	 */
    2588 	public void visitSALOAD(SALOAD o){
    2589 		indexOfInt(o, stack().peek());
    2590 		if (stack().peek(1) == Type.NULL){
    2591 			return;
    2592 		}
    2593 		if (! (stack().peek(1) instanceof ArrayType)){
    2594 			constraintViolated(o, "Stack next-to-top must be of type short[] but is '"+stack().peek(1)+"'.");
    2595 		}
    2596 		Type t = ((ArrayType) (stack().peek(1))).getBasicType();
    2597 		if (t != Type.SHORT){
    2598 			constraintViolated(o, "Stack next-to-top must be of type short[] but is '"+stack().peek(1)+"'.");
    2599 		}
    2600 	}
    2601
    2602 	/***
    2603 	 * Ensures the specific preconditions of the said instruction.
    2604 	 */
    2605 	public void visitSASTORE(SASTORE o){
    2606 		if (stack().peek() != Type.INT){
    2607 			constraintViolated(o, "The value at the stack top is not of type 'int', but of type '"+stack().peek()+"'.");
    2608 		}
    2609 		indexOfInt(o, stack().peek(1));
    2610 		if (stack().peek(2) == Type.NULL){
    2611 			return;
    2612 		}
    2613 		if (! (stack().peek(2) instanceof ArrayType)){
    2614 			constraintViolated(o, "Stack next-to-next-to-top must be of type short[] but is '"+stack().peek(2)+"'.");
    2615 		}
    2616 		Type t = ((ArrayType) (stack().peek(2))).getBasicType();
    2617 		if (t != Type.SHORT){
    2618 			constraintViolated(o, "Stack next-to-next-to-top must be of type short[] but is '"+stack().peek(2)+"'.");
    2619 		}
    2620 	}
    2621
    2622 	/***
    2623 	 * Ensures the specific preconditions of the said instruction.
    2624 	 */
    2625 	public void visitSIPUSH(SIPUSH o){
    2626 		// nothing to do here. Generic visitXXX() methods did the trick before.
    2627 	}
    2628
    2629 	/***
    2630 	 * Ensures the specific preconditions of the said instruction.
    2631 	 */
    2632 	public void visitSWAP(SWAP o){
    2633 		if (stack().peek().getSize() != 1){
    2634 			constraintViolated(o, "The value at the stack top is not of size '1', but of size '"+stack().peek().getSize()+"'.");
    2635 		}
    2636 		if (stack().peek(1).getSize() != 1){
    2637 			constraintViolated(o, "The value at the stack next-to-top is not of size '1', but of size '"+stack().peek(1).getSize()+"'.");
    2638 		}
    2639 	}
    2640
    2641 	/***
    2642 	 * Ensures the specific preconditions of the said instruction.
    2643 	 */
    2644 	public void visitTABLESWITCH(TABLESWITCH o){
    2645 		indexOfInt(o, stack().peek());
    2646 		// See Pass 3a.
    2647 	}
    2648
    2649 }
    2650

This page was automatically generated by Maven