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