View Javadoc

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