/*
 * Licensed to the Apache Software Foundation (ASF) under one
 * or more contributor license agreements.  See the NOTICE file
 * distributed with this work for additional information
 * regarding copyright ownership.  The ASF licenses this file
 * to you under the Apache License, Version 2.0 (the
 * "License"); you may not use this file except in compliance
 * with the License.  You may obtain a copy of the License at
 *
 *   https://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing,
 * software distributed under the License is distributed on an
 * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
 * KIND, either express or implied.  See the License for the
 * specific language governing permissions and limitations
 * under the License.
 */
package org.apache.bcel.verifier.structurals;

import java.util.Objects;

import org.apache.bcel.Const;
import org.apache.bcel.Repository;
import org.apache.bcel.classfile.Constant;
import org.apache.bcel.classfile.ConstantClass;
import org.apache.bcel.classfile.ConstantDouble;
import org.apache.bcel.classfile.ConstantDynamic;
import org.apache.bcel.classfile.ConstantFieldref;
import org.apache.bcel.classfile.ConstantFloat;
import org.apache.bcel.classfile.ConstantInteger;
import org.apache.bcel.classfile.ConstantLong;
import org.apache.bcel.classfile.ConstantString;
import org.apache.bcel.classfile.Field;
import org.apache.bcel.classfile.JavaClass;
//CHECKSTYLE:OFF (there are lots of references!)
import org.apache.bcel.generic.AALOAD;
import org.apache.bcel.generic.AASTORE;
import org.apache.bcel.generic.ACONST_NULL;
import org.apache.bcel.generic.ALOAD;
import org.apache.bcel.generic.ANEWARRAY;
import org.apache.bcel.generic.ARETURN;
import org.apache.bcel.generic.ARRAYLENGTH;
import org.apache.bcel.generic.ASTORE;
import org.apache.bcel.generic.ATHROW;
import org.apache.bcel.generic.ArrayType;
import org.apache.bcel.generic.BALOAD;
import org.apache.bcel.generic.BASTORE;
import org.apache.bcel.generic.BIPUSH;
import org.apache.bcel.generic.BREAKPOINT;
import org.apache.bcel.generic.BasicType;
import org.apache.bcel.generic.CALOAD;
import org.apache.bcel.generic.CASTORE;
import org.apache.bcel.generic.CHECKCAST;
import org.apache.bcel.generic.CPInstruction;
import org.apache.bcel.generic.ConstantPoolGen;
import org.apache.bcel.generic.D2F;
import org.apache.bcel.generic.D2I;
import org.apache.bcel.generic.D2L;
import org.apache.bcel.generic.DADD;
import org.apache.bcel.generic.DALOAD;
import org.apache.bcel.generic.DASTORE;
import org.apache.bcel.generic.DCMPG;
import org.apache.bcel.generic.DCMPL;
import org.apache.bcel.generic.DCONST;
import org.apache.bcel.generic.DDIV;
import org.apache.bcel.generic.DLOAD;
import org.apache.bcel.generic.DMUL;
import org.apache.bcel.generic.DNEG;
import org.apache.bcel.generic.DREM;
import org.apache.bcel.generic.DRETURN;
import org.apache.bcel.generic.DSTORE;
import org.apache.bcel.generic.DSUB;
import org.apache.bcel.generic.DUP;
import org.apache.bcel.generic.DUP2;
import org.apache.bcel.generic.DUP2_X1;
import org.apache.bcel.generic.DUP2_X2;
import org.apache.bcel.generic.DUP_X1;
import org.apache.bcel.generic.DUP_X2;
import org.apache.bcel.generic.EmptyVisitor;
import org.apache.bcel.generic.F2D;
import org.apache.bcel.generic.F2I;
import org.apache.bcel.generic.F2L;
import org.apache.bcel.generic.FADD;
import org.apache.bcel.generic.FALOAD;
import org.apache.bcel.generic.FASTORE;
import org.apache.bcel.generic.FCMPG;
import org.apache.bcel.generic.FCMPL;
import org.apache.bcel.generic.FCONST;
import org.apache.bcel.generic.FDIV;
import org.apache.bcel.generic.FLOAD;
import org.apache.bcel.generic.FMUL;
import org.apache.bcel.generic.FNEG;
import org.apache.bcel.generic.FREM;
import org.apache.bcel.generic.FRETURN;
import org.apache.bcel.generic.FSTORE;
import org.apache.bcel.generic.FSUB;
import org.apache.bcel.generic.FieldInstruction;
import org.apache.bcel.generic.GETFIELD;
import org.apache.bcel.generic.GETSTATIC;
import org.apache.bcel.generic.GOTO;
import org.apache.bcel.generic.GOTO_W;
import org.apache.bcel.generic.I2B;
import org.apache.bcel.generic.I2C;
import org.apache.bcel.generic.I2D;
import org.apache.bcel.generic.I2F;
import org.apache.bcel.generic.I2L;
import org.apache.bcel.generic.I2S;
import org.apache.bcel.generic.IADD;
import org.apache.bcel.generic.IALOAD;
import org.apache.bcel.generic.IAND;
import org.apache.bcel.generic.IASTORE;
import org.apache.bcel.generic.ICONST;
import org.apache.bcel.generic.IDIV;
import org.apache.bcel.generic.IFEQ;
import org.apache.bcel.generic.IFGE;
import org.apache.bcel.generic.IFGT;
import org.apache.bcel.generic.IFLE;
import org.apache.bcel.generic.IFLT;
import org.apache.bcel.generic.IFNE;
import org.apache.bcel.generic.IFNONNULL;
import org.apache.bcel.generic.IFNULL;
import org.apache.bcel.generic.IF_ACMPEQ;
import org.apache.bcel.generic.IF_ACMPNE;
import org.apache.bcel.generic.IF_ICMPEQ;
import org.apache.bcel.generic.IF_ICMPGE;
import org.apache.bcel.generic.IF_ICMPGT;
import org.apache.bcel.generic.IF_ICMPLE;
import org.apache.bcel.generic.IF_ICMPLT;
import org.apache.bcel.generic.IF_ICMPNE;
import org.apache.bcel.generic.IINC;
import org.apache.bcel.generic.ILOAD;
import org.apache.bcel.generic.IMPDEP1;
import org.apache.bcel.generic.IMPDEP2;
import org.apache.bcel.generic.IMUL;
import org.apache.bcel.generic.INEG;
import org.apache.bcel.generic.INSTANCEOF;
import org.apache.bcel.generic.INVOKEDYNAMIC;
import org.apache.bcel.generic.INVOKEINTERFACE;
import org.apache.bcel.generic.INVOKESPECIAL;
import org.apache.bcel.generic.INVOKESTATIC;
import org.apache.bcel.generic.INVOKEVIRTUAL;
import org.apache.bcel.generic.IOR;
import org.apache.bcel.generic.IREM;
import org.apache.bcel.generic.IRETURN;
import org.apache.bcel.generic.ISHL;
import org.apache.bcel.generic.ISHR;
import org.apache.bcel.generic.ISTORE;
import org.apache.bcel.generic.ISUB;
import org.apache.bcel.generic.IUSHR;
import org.apache.bcel.generic.IXOR;
import org.apache.bcel.generic.Instruction;
import org.apache.bcel.generic.InvokeInstruction;
import org.apache.bcel.generic.JSR;
import org.apache.bcel.generic.JSR_W;
import org.apache.bcel.generic.L2D;
import org.apache.bcel.generic.L2F;
import org.apache.bcel.generic.L2I;
import org.apache.bcel.generic.LADD;
import org.apache.bcel.generic.LALOAD;
import org.apache.bcel.generic.LAND;
import org.apache.bcel.generic.LASTORE;
import org.apache.bcel.generic.LCMP;
import org.apache.bcel.generic.LCONST;
import org.apache.bcel.generic.LDC;
import org.apache.bcel.generic.LDC2_W;
import org.apache.bcel.generic.LDC_W;
import org.apache.bcel.generic.LDIV;
import org.apache.bcel.generic.LLOAD;
import org.apache.bcel.generic.LMUL;
import org.apache.bcel.generic.LNEG;
import org.apache.bcel.generic.LOOKUPSWITCH;
import org.apache.bcel.generic.LOR;
import org.apache.bcel.generic.LREM;
import org.apache.bcel.generic.LRETURN;
import org.apache.bcel.generic.LSHL;
import org.apache.bcel.generic.LSHR;
import org.apache.bcel.generic.LSTORE;
import org.apache.bcel.generic.LSUB;
import org.apache.bcel.generic.LUSHR;
import org.apache.bcel.generic.LXOR;
import org.apache.bcel.generic.LoadClass;
import org.apache.bcel.generic.LoadInstruction;
import org.apache.bcel.generic.LocalVariableInstruction;
import org.apache.bcel.generic.MONITORENTER;
import org.apache.bcel.generic.MONITOREXIT;
import org.apache.bcel.generic.MULTIANEWARRAY;
import org.apache.bcel.generic.MethodGen;
import org.apache.bcel.generic.NEW;
import org.apache.bcel.generic.NEWARRAY;
import org.apache.bcel.generic.NOP;
import org.apache.bcel.generic.ObjectType;
import org.apache.bcel.generic.POP;
import org.apache.bcel.generic.POP2;
import org.apache.bcel.generic.PUTFIELD;
import org.apache.bcel.generic.PUTSTATIC;
import org.apache.bcel.generic.RET;
import org.apache.bcel.generic.RETURN;
import org.apache.bcel.generic.ReferenceType;
import org.apache.bcel.generic.ReturnInstruction;
import org.apache.bcel.generic.ReturnaddressType;
import org.apache.bcel.generic.SALOAD;
import org.apache.bcel.generic.SASTORE;
import org.apache.bcel.generic.SIPUSH;
import org.apache.bcel.generic.SWAP;
import org.apache.bcel.generic.StackConsumer;
import org.apache.bcel.generic.StackInstruction;
import org.apache.bcel.generic.StackProducer;
import org.apache.bcel.generic.StoreInstruction;
import org.apache.bcel.generic.TABLESWITCH;
import org.apache.bcel.generic.Type;
import org.apache.bcel.verifier.VerificationResult;
import org.apache.bcel.verifier.Verifier;
import org.apache.bcel.verifier.VerifierFactory;
import org.apache.bcel.verifier.exc.AssertionViolatedException;
import org.apache.bcel.verifier.exc.StructuralCodeConstraintException;
//CHECKSTYLE:ON

/**
 * A Visitor class testing for valid preconditions of JVM instructions. The instance of this class will throw a
 * StructuralCodeConstraintException instance if an instruction is visitXXX()ed which has preconditions that are not
 * satisfied. TODO: Currently, the JVM's behavior concerning monitors (MONITORENTER, MONITOREXIT) is not modeled in
 * JustIce.
 *
 * @see StructuralCodeConstraintException
 */
public class InstConstraintVisitor extends EmptyVisitor {

    private static final ObjectType GENERIC_ARRAY = ObjectType.getInstance(GenericArray.class.getName());

    /**
     * The Execution Frame we're working on.
     *
     * @see #setFrame(Frame f)
     * @see #locals()
     * @see #stack()
     */
    private Frame frame;

    /**
     * The ConstantPoolGen we're working on.
     *
     * @see #setConstantPoolGen(ConstantPoolGen cpg)
     */
    private ConstantPoolGen cpg;

    /**
     * The MethodGen we're working on.
     *
     * @see #setMethodGen(MethodGen mg)
     */
    private MethodGen mg;

    /**
     * The constructor. Constructs a new instance of this class.
     */
    public InstConstraintVisitor() {
    }

    /**
     * Assures arrayref is of ArrayType or NULL; returns true if and only if arrayref is non-NULL.
     *
     * @throws StructuralCodeConstraintException Thrown if the above constraint is violated.
     */
    private boolean arrayrefOfArrayType(final Instruction o, final Type arrayref) {
        if (!(arrayref instanceof ArrayType || arrayref.equals(Type.NULL))) {
            constraintViolated(o, "The 'arrayref' does not refer to an array but is of type " + arrayref + ".");
        }
        return arrayref instanceof ArrayType;
    }

    private void checkArrayElementType(final BasicType expectedElementType, final Instruction o, final Type peek) {
        if (Objects.equals(peek, Type.NULL)) {
            return;
        }
        if (!(peek instanceof ArrayType)) {
            constraintViolated(o, "Stack next-to-next-to-top must be of type " + expectedElementType + " but is '" + peek + "'.");
        }
        if (!((ArrayType) peek).isElementType(expectedElementType)) {
            constraintViolated(o, "Stack next-to-next-to-top must be of type " + expectedElementType + " but is '" + peek + "'.");
        }
    }

    private void checkTypeConstraint(final Type expected, final Instruction o, final int depth) {
        final Type peek = stack().peek(depth);
        if (!Objects.equals(expected, peek)) {
            constraintViolated(o, "The value at the stack " + depth + " from the top is not of type '" + expected + "', but of type '" + peek + "'.");
        }
    }

    private void checkTypeDoubleConstraint(final Instruction o, final int depth) {
        checkTypeConstraint(Type.DOUBLE, o, depth);
    }

    private void checkTypeFloatConstraint(final Instruction o, final int depth) {
        checkTypeConstraint(Type.FLOAT, o, depth);
    }

    private void checkTypeIntConstraint(final Instruction o, final int depth) {
        checkTypeConstraint(Type.INT, o, depth);
    }

    private void checkTypeLongConstraint(final Instruction o, final int depth) {
        checkTypeConstraint(Type.LONG, o, depth);
    }

    /**
     * This method is called by the visitXXX() to notify the acceptor of this InstConstraintVisitor that a constraint
     * violation has occurred. This is done by throwing an instance of a StructuralCodeConstraintException.
     *
     * @throws StructuralCodeConstraintException Always thrown.
     */
    private void constraintViolated(final Instruction violator, final String description) {
        final String fqClassName = violator.getClass().getName();
        throw new StructuralCodeConstraintException(
            "Instruction " + fqClassName.substring(fqClassName.lastIndexOf('.') + 1) + " constraint violated: " + description);
    }

    private ObjectType getObjectType(final FieldInstruction o) {
        final ReferenceType rt = o.getReferenceType(cpg);
        if (rt instanceof ObjectType) {
            return (ObjectType) rt;
        }
        constraintViolated(o, "expecting ObjectType but got " + rt);
        return null;
    }

    /**
     * Assures index is of type INT.
     *
     * @throws StructuralCodeConstraintException Thrown if the above constraint is not satisfied.
     */
    private void indexOfInt(final Instruction o, final Type index) {
        if (!index.equals(Type.INT)) {
            constraintViolated(o, "The 'index' is not of type int but of type " + index + ".");
        }
    }

    /**
     * The LocalVariables we're working on.
     *
     * @see #setFrame(Frame f)
     */
    private LocalVariables locals() {
        return frame.getLocals();
    }

    /**
     * Assures the ReferenceType r is initialized (or Type.NULL). Formally, this means (!(r instanceof
     * UninitializedObjectType)), because there are no uninitialized array types.
     *
     * @throws StructuralCodeConstraintException Thrown if the above constraint is not satisfied.
     */
    private void referenceTypeIsInitialized(final Instruction o, final ReferenceType r) {
        if (r instanceof UninitializedObjectType) {
            constraintViolated(o, "Working on an uninitialized object '" + r + "'.");
        }
    }

    /**
     * Sets the ConstantPoolGen instance needed for constraint checking prior to execution.
     *
     * @param cpg The constant pool generator.
     */
    public void setConstantPoolGen(final ConstantPoolGen cpg) { // TODO could be package-protected?
        this.cpg = cpg;
    }

    /**
     * This returns the single instance of the InstConstraintVisitor class. To operate correctly, other values must have
     * been set before actually using the instance. Use this method for performance reasons.
     *
     * @param f The frame to set.
     * @see #setConstantPoolGen(ConstantPoolGen cpg)
     * @see #setMethodGen(MethodGen mg)
     */
    public void setFrame(final Frame f) { // TODO could be package-protected?
        this.frame = f;
        // if (singleInstance.mg == null || singleInstance.cpg == null)
        // throw new AssertionViolatedException("Forgot to set important values first.");
    }

    /**
     * Sets the MethodGen instance needed for constraint checking prior to execution.
     *
     * @param mg The method generator.
     */
    public void setMethodGen(final MethodGen mg) {
        this.mg = mg;
    }

    /*
     * "generic"visitXXXX methods where XXXX is an interface therefore, we don't know the order of visiting; but we know these methods are called before the
     * visitYYYY methods below
     */

    /**
     * The OperandStack we're working on.
     *
     * @see #setFrame(Frame f)
     */
    private OperandStack stack() {
        return frame.getStack();
    }

    /** Assures value is of type INT. */
    private void valueOfInt(final Instruction o, final Type value) {
        if (!value.equals(Type.INT)) {
            constraintViolated(o, "The 'value' is not of type int but of type " + value + ".");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitAALOAD(final AALOAD o) {
        final Type arrayref = stack().peek(1);
        final Type index = stack().peek(0);

        indexOfInt(o, index);
        if (arrayrefOfArrayType(o, arrayref) && !(((ArrayType) arrayref).getElementType() instanceof ReferenceType)) {
            constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "
                + ((ArrayType) arrayref).getElementType() + ".");
        }
        // referenceTypeIsInitialized(o, (ReferenceType) (((ArrayType) arrayref).getElementType()));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitAASTORE(final AASTORE o) {
        final Type arrayref = stack().peek(2);
        final Type index = stack().peek(1);
        final Type value = stack().peek(0);
        indexOfInt(o, index);
        if (!(value instanceof ReferenceType)) {
            constraintViolated(o, "The 'value' is not of a ReferenceType but of type " + value + ".");
        }
        // } else {
            // referenceTypeIsInitialized(o, (ReferenceType) value);
        // }
        //
        // Don't bother further with "referenceTypeIsInitialized()", there are no arrays
        // of an uninitialized object type.
        if (arrayrefOfArrayType(o, arrayref) && !(((ArrayType) arrayref).getElementType() instanceof ReferenceType)) {
            constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "
                + ((ArrayType) arrayref).getElementType() + ".");
        }
        // No check for array element assignment compatibility. This is done at runtime.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitACONST_NULL(final ACONST_NULL o) {
        // Nothing needs to be done here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitALOAD(final ALOAD o) {
        // visitLoadInstruction(LoadInstruction) is called before.

        // Nothing else needs to be done here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitANEWARRAY(final ANEWARRAY o) {
        final Type peek = stack().peek();
        if (!peek.equals(Type.INT)) {
            constraintViolated(o, "The 'count' at the stack top is not of type '" + Type.INT + "' but of type '" + peek + "'.");
            // The runtime constant pool item at that index must be a symbolic reference to a class,
            // array, or interface type. See Pass 3a.
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitARETURN(final ARETURN o) {
        final Type peek = stack().peek();
        if (!(peek instanceof ReferenceType)) {
            constraintViolated(o, "The 'objectref' at the stack top is not of a ReferenceType but of type '" + peek + "'.");
        }
        referenceTypeIsInitialized(o, (ReferenceType) peek);

        // The check below should already done via visitReturnInstruction(ReturnInstruction), see there.
        // It cannot be done using Staerk-et-al's "set of object types" instead of a
        // "wider cast object type", anyway.
        // if (! objectref.isAssignmentCompatibleWith(mg.getReturnType() )) {
        // constraintViolated(o, "The 'objectref' type "+objectref+
        // " at the stack top is not assignment compatible with the return type '"+mg.getReturnType()+"' of the method.");
        // }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitARRAYLENGTH(final ARRAYLENGTH o) {
        arrayrefOfArrayType(o, stack().peek(0));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitASTORE(final ASTORE o) {
        final Type peek = stack().peek();
        if (!(peek instanceof ReferenceType || peek instanceof ReturnaddressType)) {
            constraintViolated(o, "The 'objectref' is not of a ReferenceType or of ReturnaddressType but of " + peek + ".");
        }
        // if (stack().peek() instanceof ReferenceType) {
        // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
        // }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitATHROW(final ATHROW o) {
        try {
            // It's stated that 'objectref' must be of a ReferenceType --- but since Throwable is
            // not derived from an ArrayType, it follows that 'objectref' must be of an ObjectType or Type.NULL.
            final Type peek = stack().peek();
            if (!(peek instanceof ObjectType || peek.equals(Type.NULL))) {
                constraintViolated(o, "The 'objectref' is not of an (initialized) ObjectType but of type " + peek + ".");
            }
            // NULL is a subclass of every class, so to speak.
            if (peek.equals(Type.NULL)) {
                return;
            }
            final ObjectType exc = (ObjectType) peek;
            final ObjectType throwable = (ObjectType) Type.getType("Ljava/lang/Throwable;");
            if (!exc.subclassOf(throwable) && !exc.equals(throwable)) {
                constraintViolated(o, "The 'objectref' is not of class Throwable or of a subclass of Throwable, but of '" + peek + "'.");
            }
        } catch (final ClassNotFoundException e) {
            // FIXME: maybe not the best way to handle this
            throw new AssertionViolatedException("Missing class: " + e, e);
        }
    }

    /*
    /* "special"visitXXXX methods for one type of instruction each.
     */

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitBALOAD(final BALOAD o) {
        final Type arrayref = stack().peek(1);
        final Type index = stack().peek(0);
        indexOfInt(o, index);
        if (arrayrefOfArrayType(o, arrayref)
            && !(((ArrayType) arrayref).isElementType(Type.BOOLEAN) || ((ArrayType) arrayref).isElementType(Type.BYTE))) {
            constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"
                + ((ArrayType) arrayref).getElementType() + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitBASTORE(final BASTORE o) {
        final Type arrayref = stack().peek(2);
        final Type index = stack().peek(1);
        final Type value = stack().peek(0);
        indexOfInt(o, index);
        valueOfInt(o, value);
        if (arrayrefOfArrayType(o, arrayref)
            && !(((ArrayType) arrayref).isElementType(Type.BOOLEAN) || ((ArrayType) arrayref).isElementType(Type.BYTE))) {
            constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"
                + ((ArrayType) arrayref).getElementType() + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitBIPUSH(final BIPUSH o) {
        // Nothing to do...
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitBREAKPOINT(final BREAKPOINT o) {
        throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as BREAKPOINT.");
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitCALOAD(final CALOAD o) {
        final Type arrayref = stack().peek(1);
        final Type index = stack().peek(0);
        indexOfInt(o, index);
        if (arrayrefOfArrayType(o, arrayref) && !((ArrayType) arrayref).isElementType(Type.CHAR)) {
            constraintViolated(o, "The 'arrayref' does not refer to an array with elements of type char but to an array of type "
                + ((ArrayType) arrayref).getElementType() + ".");
        }
    }

    /*
     * "generic" visitYYYY methods where YYYY is a superclass.
     * therefore, we know the order of visiting; we know
     * these methods are called after the visitXXXX methods above.
     */

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitCASTORE(final CASTORE o) {
        final Type arrayref = stack().peek(2);
        final Type index = stack().peek(1);
        final Type value = stack().peek(0);
        indexOfInt(o, index);
        valueOfInt(o, value);
        if (arrayrefOfArrayType(o, arrayref) && !((ArrayType) arrayref).isElementType(Type.CHAR)) {
            constraintViolated(o, "The 'arrayref' does not refer to an array with elements of type char but to an array of type "
                + ((ArrayType) arrayref).getElementType() + ".");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitCHECKCAST(final CHECKCAST o) {
        // The objectref must be of type reference.
        final Type objectref = stack().peek(0);
        if (!(objectref instanceof ReferenceType)) {
            constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type " + objectref + ".");
        }
        // else{
        // referenceTypeIsInitialized(o, (ReferenceType) objectref);
        // }
        // The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
        // current class (�3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
        // pool item at the index must be a symbolic reference to a class, array, or interface type.
        final Constant c = cpg.getConstant(o.getIndex());
        if (!(c instanceof ConstantClass)) {
            constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '" + c + "'.");
        }
    }

    /**
     * Ensures the general preconditions of a CPInstruction instance.
     */
    @Override
    public void visitCPInstruction(final CPInstruction o) {
        final int idx = o.getIndex();
        if (idx < 0 || idx >= cpg.getSize()) {
            throw new AssertionViolatedException("Huh?! Constant pool index of instruction '" + o + "' illegal? Pass 3a should have checked this.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitD2F(final D2F o) {
        checkTypeDoubleConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitD2I(final D2I o) {
        checkTypeDoubleConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitD2L(final D2L o) {
        checkTypeDoubleConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDADD(final DADD o) {
        checkTypeDoubleConstraint(o, 0);
        checkTypeDoubleConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDALOAD(final DALOAD o) {
        indexOfInt(o, stack().peek());
        checkArrayElementType(Type.DOUBLE, o, stack().peek(1));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDASTORE(final DASTORE o) {
        checkTypeDoubleConstraint(o, 0);
        indexOfInt(o, stack().peek(1));
        checkArrayElementType(Type.DOUBLE, o, stack().peek(2));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDCMPG(final DCMPG o) {
        checkTypeDoubleConstraint(o, 0);
        checkTypeDoubleConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDCMPL(final DCMPL o) {
        checkTypeDoubleConstraint(o, 0);
        checkTypeDoubleConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDCONST(final DCONST o) {
        // There's nothing to be done here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDDIV(final DDIV o) {
        checkTypeDoubleConstraint(o, 0);
        checkTypeDoubleConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDLOAD(final DLOAD o) {
        // visitLoadInstruction(LoadInstruction) is called before.

        // Nothing else needs to be done here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDMUL(final DMUL o) {
        checkTypeDoubleConstraint(o, 0);
        checkTypeDoubleConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDNEG(final DNEG o) {
        checkTypeDoubleConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDREM(final DREM o) {
        checkTypeDoubleConstraint(o, 0);
        checkTypeDoubleConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDRETURN(final DRETURN o) {
        checkTypeDoubleConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDSTORE(final DSTORE o) {
        // visitStoreInstruction(StoreInstruction) is called before.

        // Nothing else needs to be done here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDSUB(final DSUB o) {
        checkTypeDoubleConstraint(o, 0);
        checkTypeDoubleConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDUP(final DUP o) {
        final Type peek = stack().peek();
        if (peek.getSize() != 1) {
            constraintViolated(o,
                "Won't DUP type on stack top '" + peek + "' because it must occupy exactly one slot, not '" + peek.getSize() + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDUP_X1(final DUP_X1 o) {
        final Type peek = stack().peek();
        if (peek.getSize() != 1) {
            constraintViolated(o, "Type on stack top '" + peek + "' should occupy exactly one slot, not '" + peek.getSize() + "'.");
        }
        final Type peek1 = stack().peek(1);
        if (peek1.getSize() != 1) {
            constraintViolated(o,
                "Type on stack next-to-top '" + peek1 + "' should occupy exactly one slot, not '" + peek1.getSize() + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDUP_X2(final DUP_X2 o) {
        final Type peek = stack().peek();
        if (peek.getSize() != 1) {
            constraintViolated(o, "Stack top type must be of size 1, but is '" + peek + "' of size '" + peek.getSize() + "'.");
        }
        final Type peek1 = stack().peek(1);
        if (peek1.getSize() == 2) {
            return; // Form 2, okay.
        }
        // stack().peek(1).getSize == 1.
        final Type peek2 = stack().peek(2);
        if (peek2.getSize() != 1) {
            constraintViolated(o, "If stack top's size is 1 and stack next-to-top's size is 1, stack next-to-next-to-top's size must also be 1, but is: '"
                + peek2 + "' of size '" + peek2.getSize() + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDUP2(final DUP2 o) {
        final Type peek = stack().peek();
        if (peek.getSize() == 2) {
            return; // Form 2, okay.
        }
        // stack().peek().getSize() == 1.
        final Type peek1 = stack().peek(1);
        if (peek1.getSize() != 1) {
            constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '" + peek1 + "' of size '"
                + peek1.getSize() + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDUP2_X1(final DUP2_X1 o) {
        final Type peek = stack().peek();
        final Type peek1 = stack().peek(1);
        if (peek.getSize() == 2) {
            if (peek1.getSize() != 1) {
                constraintViolated(o, "If stack top's size is 2, then stack next-to-top's size must be 1. But it is '" + peek1 + "' of size '"
                    + peek1.getSize() + "'.");
            }
        } else { // stack top is of size 1
            if (peek1.getSize() != 1) {
                constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '" + peek1 + "' of size '"
                    + peek1.getSize() + "'.");
            }
            final Type peek2 = stack().peek(2);
            if (peek2.getSize() != 1) {
                constraintViolated(o, "If stack top's size is 1, then stack next-to-next-to-top's size must also be 1. But it is '" + peek2
                    + "' of size '" + peek2.getSize() + "'.");
            }
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitDUP2_X2(final DUP2_X2 o) {
        final Type peek = stack().peek(0);
        final Type peek1 = stack().peek(1);
        final Type peek2 = stack().peek(2);
        if (peek.getSize() == 2) {
            // stack top size is 2, next-to-top's size is 1
            if (peek1.getSize() == 2 || peek2.getSize() == 1) {
                return; // Form 2
            }
            constraintViolated(o, "If stack top's size is 2 and stack-next-to-top's size is 1,"
                + " then stack next-to-next-to-top's size must also be 1. But it is '" + peek2 + "' of size '" + peek2.getSize() + "'.");
        } else if (peek1.getSize() == 1 && (peek2.getSize() == 2 || stack().peek(3).getSize() == 1)) {
            return; // Form 1
        }
        constraintViolated(o, "The operand sizes on the stack do not match any of the four forms of usage of this instruction.");
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitF2D(final F2D o) {
        checkTypeFloatConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitF2I(final F2I o) {
        checkTypeFloatConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitF2L(final F2L o) {
        checkTypeFloatConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFADD(final FADD o) {
        checkTypeFloatConstraint(o, 0);
        checkTypeFloatConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFALOAD(final FALOAD o) {
        indexOfInt(o, stack().peek());
        checkArrayElementType(Type.FLOAT, o, stack().peek(1));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFASTORE(final FASTORE o) {
        checkTypeFloatConstraint(o, 0);
        indexOfInt(o, stack().peek(1));
        checkArrayElementType(Type.FLOAT, o, stack().peek(2));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFCMPG(final FCMPG o) {
        checkTypeFloatConstraint(o, 0);
        checkTypeFloatConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFCMPL(final FCMPL o) {
        checkTypeFloatConstraint(o, 0);
        checkTypeFloatConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFCONST(final FCONST o) {
        // nothing to do here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFDIV(final FDIV o) {
        checkTypeFloatConstraint(o, 0);
        checkTypeFloatConstraint(o, 1);
    }

    /**
     * Ensures the general preconditions of a FieldInstruction instance.
     */
    @Override
    public void visitFieldInstruction(final FieldInstruction o) {
        // visitLoadClass(o) has been called before: Every FieldOrMethod
        // implements LoadClass.
        // visitCPInstruction(o) has been called before.
        // A FieldInstruction may be: GETFIELD, GETSTATIC, PUTFIELD, PUTSTATIC
        final Constant c = cpg.getConstant(o.getIndex());
        if (!(c instanceof ConstantFieldref)) {
            constraintViolated(o, "Index '" + o.getIndex() + "' should refer to a CONSTANT_Fieldref_info structure, but refers to '" + c + "'.");
        }
        // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
        final Type t = o.getType(cpg);
        if (t instanceof ObjectType) {
            final String name = ((ObjectType) t).getClassName();
            final Verifier v = VerifierFactory.getVerifier(name);
            final VerificationResult vr = v.doPass2();
            if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
                constraintViolated(o, "Class '" + name + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
            }
        }
    }

    private Field visitFieldInstructionInternals(final FieldInstruction o) throws ClassNotFoundException {
        final String fieldName = o.getFieldName(cpg);
        final JavaClass jc = Repository.lookupClass(getObjectType(o).getClassName());
        final Field f = jc.findField(fieldName, o.getType(cpg));
        if (f == null) {
            throw new AssertionViolatedException("Field '" + fieldName + "' not found in " + jc.getClassName());
        }
        final Type value = stack().peek();
        final Type t = Type.getType(f.getSignature());
        Type shouldBe = t;
        if (shouldBe == Type.BOOLEAN || shouldBe == Type.BYTE || shouldBe == Type.CHAR || shouldBe == Type.SHORT) {
            shouldBe = Type.INT;
        }
        if (t instanceof ReferenceType) {
            if (value instanceof ReferenceType) {
                final ReferenceType rValue = (ReferenceType) value;
                referenceTypeIsInitialized(o, rValue);
                // TODO: This can possibly only be checked using Staerk-et-al's "set-of-object types", not
                // using "wider cast object types" created during verification.
                // Comment it out if you encounter problems. See also the analogon at visitPUTFIELD|visitPUTSTATIC.
                if (!rValue.isAssignmentCompatibleWith(shouldBe)) {
                    constraintViolated(o, "The stack top type '" + value + "' is not assignment compatible with '" + shouldBe + "'.");
                }
            } else {
                constraintViolated(o, "The stack top type '" + value + "' is not of a reference type as expected.");
            }
        } else if (shouldBe != value) {
            constraintViolated(o, "The stack top type '" + value + "' is not of type '" + shouldBe + "' as expected.");
        }
        return f;
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFLOAD(final FLOAD o) {
        // visitLoadInstruction(LoadInstruction) is called before.

        // Nothing else needs to be done here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFMUL(final FMUL o) {
        checkTypeFloatConstraint(o, 0);
        checkTypeFloatConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFNEG(final FNEG o) {
        checkTypeFloatConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFREM(final FREM o) {
        checkTypeFloatConstraint(o, 0);
        checkTypeFloatConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFRETURN(final FRETURN o) {
        checkTypeFloatConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFSTORE(final FSTORE o) {
        // visitStoreInstruction(StoreInstruction) is called before.

        // Nothing else needs to be done here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitFSUB(final FSUB o) {
        checkTypeFloatConstraint(o, 0);
        checkTypeFloatConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitGETFIELD(final GETFIELD o) {
        try {
            final Type objectref = stack().peek();
            if (!(objectref instanceof ObjectType || objectref == Type.NULL)) {
                constraintViolated(o, "Stack top should be an object reference that's not an array reference, but is '" + objectref + "'.");
            }
            final String fieldName = o.getFieldName(cpg);

            final JavaClass jc = Repository.lookupClass(getObjectType(o).getClassName());
            final Field f = jc.findField(fieldName, o.getType(cpg));
            if (f == null) {
                throw new AssertionViolatedException("Field '" + fieldName + "' not found in " + jc.getClassName());
            }
            if (f.isProtected()) {
                final ObjectType classtype = getObjectType(o);
                final ObjectType curr = ObjectType.getInstance(mg.getClassName());
                if (classtype.equals(curr) || curr.subclassOf(classtype)) {
                    final Type t = stack().peek();
                    if (t == Type.NULL) {
                        return;
                    }
                    if (!(t instanceof ObjectType)) {
                        constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '" + t + "'.");
                    }
                    // final ObjectType objreftype = (ObjectType) t;
                    // if (!(objreftype.equals(curr) || objreftype.subclassOf(curr))) {
                        // TODO: One day move to Staerk-et-al's "Set of object types" instead of "wider" object types
                        // created during the verification.
                        // "Wider" object types don't allow us to check for things like that below.
                        // constraintViolated(o, "The referenced field has the ACC_PROTECTED modifier, "+
                        // "and it's a member of the current class or a superclass of the current class."+
                        // " However, the referenced object type '"+stack().peek()+
                        // "' is not the current class or a subclass of the current class.");
                    //}
                }
            }
            // TODO: Could go into Pass 3a.
            if (f.isStatic()) {
                constraintViolated(o, "Referenced field '" + f + "' is static which it shouldn't be.");
            }
        } catch (final ClassNotFoundException e) {
            // FIXME: maybe not the best way to handle this
            throw new AssertionViolatedException("Missing class: " + e, e);
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitGETSTATIC(final GETSTATIC o) {
        // Field must be static: see Pass 3a.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitGOTO(final GOTO o) {
        // nothing to do here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitGOTO_W(final GOTO_W o) {
        // nothing to do here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitI2B(final I2B o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitI2C(final I2C o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitI2D(final I2D o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitI2F(final I2F o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitI2L(final I2L o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitI2S(final I2S o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIADD(final IADD o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIALOAD(final IALOAD o) {
        indexOfInt(o, stack().peek());
        checkArrayElementType(Type.INT, o, stack().peek(1));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIAND(final IAND o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIASTORE(final IASTORE o) {
        checkTypeIntConstraint(o, 0);
        indexOfInt(o, stack().peek(1));
        checkArrayElementType(Type.INT, o, stack().peek(2));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitICONST(final ICONST o) {
        // nothing to do here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIDIV(final IDIV o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIF_ACMPEQ(final IF_ACMPEQ o) {
        if (!(stack().peek() instanceof ReferenceType)) {
            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
        }
        // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
        if (!(stack().peek(1) instanceof ReferenceType)) {
            constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '" + stack().peek(1) + "'.");
        }
        // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) );
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIF_ACMPNE(final IF_ACMPNE o) {
        if (!(stack().peek() instanceof ReferenceType)) {
            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
            // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
        }
        if (!(stack().peek(1) instanceof ReferenceType)) {
            constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '" + stack().peek(1) + "'.");
            // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) );
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIF_ICMPEQ(final IF_ICMPEQ o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIF_ICMPGE(final IF_ICMPGE o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIF_ICMPGT(final IF_ICMPGT o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIF_ICMPLE(final IF_ICMPLE o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIF_ICMPLT(final IF_ICMPLT o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIF_ICMPNE(final IF_ICMPNE o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIFEQ(final IFEQ o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIFGE(final IFGE o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIFGT(final IFGT o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIFLE(final IFLE o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIFLT(final IFLT o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIFNE(final IFNE o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIFNONNULL(final IFNONNULL o) {
        if (!(stack().peek() instanceof ReferenceType)) {
            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
        }
        referenceTypeIsInitialized(o, (ReferenceType) stack().peek());
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIFNULL(final IFNULL o) {
        if (!(stack().peek() instanceof ReferenceType)) {
            constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
        }
        referenceTypeIsInitialized(o, (ReferenceType) stack().peek());
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIINC(final IINC o) {
        // Mhhh. In BCEL, at this time "IINC" is not a LocalVariableInstruction.
        if (locals().maxLocals() <= (o.getType(cpg).getSize() == 1 ? o.getIndex() : o.getIndex() + 1)) {
            constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
        }
        indexOfInt(o, locals().get(o.getIndex()));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitILOAD(final ILOAD o) {
        // All done by visitLocalVariableInstruction(), visitLoadInstruction()
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIMPDEP1(final IMPDEP1 o) {
        throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP1.");
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIMPDEP2(final IMPDEP2 o) {
        throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP2.");
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIMUL(final IMUL o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitINEG(final INEG o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitINSTANCEOF(final INSTANCEOF o) {
        // The objectref must be of type reference.
        final Type objectref = stack().peek(0);
        if (!(objectref instanceof ReferenceType)) {
            constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type " + objectref + ".");
        }
        // else{
        // referenceTypeIsInitialized(o, (ReferenceType) objectref);
        // }
        // The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
        // current class (�3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
        // pool item at the index must be a symbolic reference to a class, array, or interface type.
        final Constant c = cpg.getConstant(o.getIndex());
        if (!(c instanceof ConstantClass)) {
            constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '" + c + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     *
     * @since 6.0
     */
    @Override
    public void visitINVOKEDYNAMIC(final INVOKEDYNAMIC o) {
        throw new UnsupportedOperationException("INVOKEDYNAMIC instruction is not supported at this time");
    }

    /**
     * Ensures the general preconditions of an InvokeInstruction instance.
     */
    @Override
    public void visitInvokeInstruction(final InvokeInstruction o) {
        // visitLoadClass(o) has been called before: Every FieldOrMethod
        // implements LoadClass.
        // visitCPInstruction(o) has been called before.
        // TODO
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitINVOKEINTERFACE(final INVOKEINTERFACE o) {
        // Method is not native, otherwise pass 3 would not happen.
        final int count = o.getCount();
        if (count == 0) {
            constraintViolated(o, "The 'count' argument must not be 0.");
        }
        // It is a ConstantInterfaceMethodref, Pass 3a made it sure.
        // TODO: Do we want to do anything with it?
        // ConstantInterfaceMethodref cimr = (ConstantInterfaceMethodref) (cpg.getConstant(o.getIndex()));
        // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
        final Type t = o.getType(cpg);
        if (t instanceof ObjectType) {
            final String name = ((ObjectType) t).getClassName();
            final Verifier v = VerifierFactory.getVerifier(name);
            final VerificationResult vr = v.doPass2();
            if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
                constraintViolated(o, "Class '" + name + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
            }
        }
        final Type[] argTypes = o.getArgumentTypes(cpg);
        final int argCount = argTypes.length;
        for (int i = argCount - 1; i >= 0; i--) {
            final Type fromStack = stack().peek(argCount - 1 - i); // 0 to argCount - 1
            Type fromDesc = argTypes[i];
            if (fromDesc == Type.BOOLEAN || fromDesc == Type.BYTE || fromDesc == Type.CHAR || fromDesc == Type.SHORT) {
                fromDesc = Type.INT;
            }
            if (!fromStack.equals(fromDesc)) {
                if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType) {
                    final ReferenceType rFromStack = (ReferenceType) fromStack;
                    // ReferenceType rFromDesc = (ReferenceType) fromDesc;
                    // TODO: This can only be checked when using Staerk-et-al's "set of object types"
                    // instead of a "wider cast object type" created during verification.
                    // if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ) {
                    // constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+
                    // "' on the stack (which is not assignment compatible).");
                    // }
                    referenceTypeIsInitialized(o, rFromStack);
                } else {
                    constraintViolated(o, "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack.");
                }
            }
        }
        Type objRef = stack().peek(argCount);
        if (objRef == Type.NULL) {
            return;
        }
        if (!(objRef instanceof ReferenceType)) {
            constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '" + objRef + "'.");
        }
        referenceTypeIsInitialized(o, (ReferenceType) objRef);
        if (!(objRef instanceof ObjectType)) {
            if (!(objRef instanceof ArrayType)) { // could be a ReturnaddressType
                constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '" + objRef + "'.");
            } else {
                objRef = GENERIC_ARRAY;
            }
        }
        // String objRefClassName = ((ObjectType) objRef).getClassName();
        // String theInterface = o.getClassName(cpg);
        // TODO: This can only be checked if we're using Staerk-et-al's "set of object types"
        // instead of "wider cast object types" generated during verification.
        // if ( ! Repository.implementationOf(objRefClassName, theInterface) ) {
        // constraintViolated(o, "The 'objRef' item '" + objRef + "' does not implement '" + theInterface + "' as expected.");
        // }
        int countedCount = 1; // 1 for the objectref
        for (int i = 0; i < argCount; i++) {
            countedCount += argTypes[i].getSize();
        }
        if (count != countedCount) {
            constraintViolated(o, "The 'count' argument should probably read '" + countedCount + "' but is '" + count + "'.");
        }
    }

    private int visitInvokeInternals(final InvokeInstruction o) throws ClassNotFoundException {
        final Type t = o.getType(cpg);
        if (t instanceof ObjectType) {
            final String name = ((ObjectType) t).getClassName();
            final Verifier v = VerifierFactory.getVerifier(name);
            final VerificationResult vr = v.doPass2();
            if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
                constraintViolated(o, "Class '" + name + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
            }
        }
        final Type[] argtypes = o.getArgumentTypes(cpg);
        final int nargs = argtypes.length;

        for (int i = nargs - 1; i >= 0; i--) {
            final Type fromStack = stack().peek(nargs - 1 - i); // 0 to nargs-1
            Type fromDesc = argtypes[i];
            if (fromDesc == Type.BOOLEAN || fromDesc == Type.BYTE || fromDesc == Type.CHAR || fromDesc == Type.SHORT) {
                fromDesc = Type.INT;
            }
            if (!fromStack.equals(fromDesc)) {
                if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType) {
                    final ReferenceType rFromStack = (ReferenceType) fromStack;
                    final ReferenceType rFromDesc = (ReferenceType) fromDesc;
                    // TODO: This can possibly only be checked when using Staerk-et-al's "set of object types" instead
                    // of a single "wider cast object type" created during verification.
                    if (!rFromStack.isAssignmentCompatibleWith(rFromDesc)) {
                        constraintViolated(o,
                            "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack (which is not assignment compatible).");
                    }
                    referenceTypeIsInitialized(o, rFromStack);
                } else {
                    constraintViolated(o, "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack.");
                }
            }
        }
        return nargs;
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitINVOKESPECIAL(final INVOKESPECIAL o) {
        try {
            // Don't init an object twice.
            if (o.getMethodName(cpg).equals(Const.CONSTRUCTOR_NAME) && !(stack().peek(o.getArgumentTypes(cpg).length) instanceof UninitializedObjectType)) {
                constraintViolated(o,
                    "Possibly initializing object twice."
                        + " A valid instruction sequence must not have an uninitialized object on the operand stack or in a local variable"
                        + " during a backwards branch, or in a local variable in code protected by an exception handler."
                        + " Please see The Java Virtual Machine Specification, Second Edition, 4.9.4 (pages 147 and 148) for details.");
            }
            // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
            final int nargs = visitInvokeInternals(o);
            Type objref = stack().peek(nargs);
            if (objref == Type.NULL) {
                return;
            }
            if (!(objref instanceof ReferenceType)) {
                constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '" + objref + "'.");
            }
            String objRefClassName = null;
            if (!o.getMethodName(cpg).equals(Const.CONSTRUCTOR_NAME)) {
                referenceTypeIsInitialized(o, (ReferenceType) objref);
                if (!(objref instanceof ObjectType)) {
                    if (!(objref instanceof ArrayType)) { // could be a ReturnaddressType
                        constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '" + objref + "'.");
                    } else {
                        objref = GENERIC_ARRAY;
                    }
                }

                objRefClassName = ((ObjectType) objref).getClassName();
            } else {
                if (!(objref instanceof UninitializedObjectType)) {
                    constraintViolated(o, "Expecting an UninitializedObjectType as 'objectref' on the stack, not a '" + objref
                        + "'. Otherwise, you couldn't invoke a method since an array has no methods (not to speak of a return address).");
                }
                objRefClassName = ((UninitializedObjectType) objref).getInitialized().getClassName();
            }

            final String theClass = o.getClassName(cpg);
            if (!Repository.instanceOf(objRefClassName, theClass)) {
                constraintViolated(o, "The 'objref' item '" + objref + "' does not implement '" + theClass + "' as expected.");
            }

        } catch (final ClassNotFoundException e) {
            // FIXME: maybe not the best way to handle this
            throw new AssertionViolatedException("Missing class: " + e, e);
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitINVOKESTATIC(final INVOKESTATIC o) {
        try {
            // Method is not native, otherwise pass 3 would not happen.
            visitInvokeInternals(o);
        } catch (final ClassNotFoundException e) {
            // FIXME: maybe not the best way to handle this
            throw new AssertionViolatedException("Missing class: " + e, e);
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitINVOKEVIRTUAL(final INVOKEVIRTUAL o) {
        try {
            // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).

            final int nargs = visitInvokeInternals(o);
            Type objref = stack().peek(nargs);
            if (objref == Type.NULL) {
                return;
            }
            if (!(objref instanceof ReferenceType)) {
                constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '" + objref + "'.");
            }
            referenceTypeIsInitialized(o, (ReferenceType) objref);
            if (!(objref instanceof ObjectType)) {
                if (!(objref instanceof ArrayType)) { // could be a ReturnaddressType
                    constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '" + objref + "'.");
                } else {
                    objref = GENERIC_ARRAY;
                }
            }
            final String objRefClassName = ((ObjectType) objref).getClassName();
            final String theClass = o.getClassName(cpg);
            if (objref != GENERIC_ARRAY && !Repository.instanceOf(objRefClassName, theClass)) {
                constraintViolated(o, "The 'objref' item '" + objref + "' does not implement '" + theClass + "' as expected.");
            }
        } catch (final ClassNotFoundException e) {
            // FIXME: maybe not the best way to handle this
            throw new AssertionViolatedException("Missing class: " + e, e);
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIOR(final IOR o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIREM(final IREM o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIRETURN(final IRETURN o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitISHL(final ISHL o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitISHR(final ISHR o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitISTORE(final ISTORE o) {
        // visitStoreInstruction(StoreInstruction) is called before.
        // Nothing else needs to be done here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitISUB(final ISUB o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIUSHR(final IUSHR o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitIXOR(final IXOR o) {
        checkTypeIntConstraint(o, 0);
        checkTypeIntConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitJSR(final JSR o) {
        // nothing to do here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitJSR_W(final JSR_W o) {
        // nothing to do here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitL2D(final L2D o) {
        checkTypeLongConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitL2F(final L2F o) {
        checkTypeLongConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitL2I(final L2I o) {
        checkTypeLongConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLADD(final LADD o) {
        checkTypeLongConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLALOAD(final LALOAD o) {
        indexOfInt(o, stack().peek());
        checkArrayElementType(Type.LONG, o, stack().peek(1));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLAND(final LAND o) {
        checkTypeLongConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLASTORE(final LASTORE o) {
        checkTypeLongConstraint(o, 0);
        indexOfInt(o, stack().peek(1));
        checkArrayElementType(Type.LONG, o, stack().peek(2));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLCMP(final LCMP o) {
        checkTypeLongConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLCONST(final LCONST o) {
        // Nothing to do here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLDC(final LDC o) {
        // visitCPInstruction is called first.

        final Constant c = cpg.getConstant(o.getIndex());
        if (!(c instanceof ConstantInteger
                || c instanceof ConstantFloat
                || c instanceof ConstantString
                || c instanceof ConstantClass
                || c instanceof ConstantDynamic)) {
            constraintViolated(o,
                "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float, a CONSTANT_String, a CONSTANT_Class, or a CONSTANT_Dynamic but is '"
                        + c + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     *
     * @param o The instruction to visit.
     */
    public void visitLDC_W(final LDC_W o) {
        // visitCPInstruction is called first.

        final Constant c = cpg.getConstant(o.getIndex());
        if (!(c instanceof ConstantInteger || c instanceof ConstantFloat || c instanceof ConstantString || c instanceof ConstantClass)) {
            constraintViolated(o,
                "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float, a CONSTANT_String or a CONSTANT_Class, but is '" + c + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLDC2_W(final LDC2_W o) {
        // visitCPInstruction is called first.

        final Constant c = cpg.getConstant(o.getIndex());
        if (!(c instanceof ConstantLong || c instanceof ConstantDouble)) {
            constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '" + c + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLDIV(final LDIV o) {
        checkTypeLongConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLLOAD(final LLOAD o) {
        // visitLoadInstruction(LoadInstruction) is called before.

        // Nothing else needs to be done here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLMUL(final LMUL o) {
        checkTypeLongConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLNEG(final LNEG o) {
        checkTypeLongConstraint(o, 0);
    }

    /**
     * Assures the generic preconditions of a LoadClass instance. The referenced class is loaded and pass2-verified.
     */
    @Override
    public void visitLoadClass(final LoadClass o) {
        final ObjectType t = o.getLoadClassType(cpg);
        if (t != null) { // null means "no class is loaded"
            final Verifier v = VerifierFactory.getVerifier(t.getClassName());
            final VerificationResult vr = v.doPass2();
            if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
                constraintViolated((Instruction) o,
                    "Class '" + o.getLoadClassType(cpg).getClassName() + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
            }
        }
    }

    /**
     * Assures the generic preconditions of a LoadInstruction instance.
     */
    @Override
    public void visitLoadInstruction(final LoadInstruction o) {
        // visitLocalVariableInstruction(o) is called before, because it is more generic.

        // LOAD instructions must not read Type.UNKNOWN
        if (locals().get(o.getIndex()) == Type.UNKNOWN) {
            constraintViolated(o, "Read-Access on local variable " + o.getIndex() + " with unknown content.");
        }

        // LOAD instructions, two-slot-values at index N must have Type.UNKNOWN
        // as a symbol for the higher halve at index N+1
        // [suppose some instruction put an int at N+1--- our double at N is defective]
        if (o.getType(cpg).getSize() == 2 && locals().get(o.getIndex() + 1) != Type.UNKNOWN) {
            constraintViolated(o,
                "Reading a two-locals value from local variables " + o.getIndex() + " and " + (o.getIndex() + 1) + " where the latter one is destroyed.");
        }

        // LOAD instructions must read the correct type.
        if (!(o instanceof ALOAD)) {
            if (locals().get(o.getIndex()) != o.getType(cpg)) {
                constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '" + locals().get(o.getIndex())
                    + "'; Instruction type: '" + o.getType(cpg) + "'.");
            }
        } else if (!(locals().get(o.getIndex()) instanceof ReferenceType)) {
            constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '" + locals().get(o.getIndex())
                + "'; Instruction expects a ReferenceType.");
        }
        // ALOAD __IS ALLOWED__ to put uninitialized objects onto the stack!
        // referenceTypeIsInitialized(o, (ReferenceType) (locals().get(o.getIndex())));

        // LOAD instructions must have enough free stack slots.
        if (stack().maxStack() - stack().slotsUsed() < o.getType(cpg).getSize()) {
            constraintViolated(o, "Not enough free stack slots to load a '" + o.getType(cpg) + "' onto the OperandStack.");
        }
    }

    /**
     * Assures the generic preconditions of a LocalVariableInstruction instance. That is, the index of the local variable
     * must be valid.
     */
    @Override
    public void visitLocalVariableInstruction(final LocalVariableInstruction o) {
        if (locals().maxLocals() <= (o.getType(cpg).getSize() == 1 ? o.getIndex() : o.getIndex() + 1)) {
            constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLOOKUPSWITCH(final LOOKUPSWITCH o) {
        checkTypeIntConstraint(o, 0);
        // See also pass 3a.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLOR(final LOR o) {
        checkTypeLongConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLREM(final LREM o) {
        checkTypeLongConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLRETURN(final LRETURN o) {
        checkTypeLongConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLSHL(final LSHL o) {
        checkTypeIntConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLSHR(final LSHR o) {
        checkTypeIntConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLSTORE(final LSTORE o) {
        // visitStoreInstruction(StoreInstruction) is called before.

        // Nothing else needs to be done here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLSUB(final LSUB o) {
        checkTypeLongConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLUSHR(final LUSHR o) {
        checkTypeIntConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitLXOR(final LXOR o) {
        checkTypeLongConstraint(o, 0);
        checkTypeLongConstraint(o, 1);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitMONITORENTER(final MONITORENTER o) {
        if (!(stack().peek() instanceof ReferenceType)) {
            constraintViolated(o, "The stack top should be of a ReferenceType, but is '" + stack().peek() + "'.");
        }
        // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitMONITOREXIT(final MONITOREXIT o) {
        if (!(stack().peek() instanceof ReferenceType)) {
            constraintViolated(o, "The stack top should be of a ReferenceType, but is '" + stack().peek() + "'.");
        }
        // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitMULTIANEWARRAY(final MULTIANEWARRAY o) {
        final int dimensions = o.getDimensions();
        // Dimensions argument is okay: see Pass 3a.
        for (int i = 0; i < dimensions; i++) {
            if (stack().peek(i) != Type.INT) {
                constraintViolated(o, "The '" + dimensions + "' upper stack types should be 'int' but aren't.");
            }
        }
        // The runtime constant pool item at that index must be a symbolic reference to a class,
        // array, or interface type. See Pass 3a.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitNEW(final NEW o) {
        // visitCPInstruction(CPInstruction) has been called before.
        // visitLoadClass(LoadClass) has been called before.

        final Type t = o.getType(cpg);
        if (!(t instanceof ReferenceType)) {
            throw new AssertionViolatedException("NEW.getType() returning a non-reference type?.");
        }
        if (!(t instanceof ObjectType)) {
            constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '" + t + "'.");
        }
        final ObjectType obj = (ObjectType) t;

        // for example: Don't instantiate interfaces
        try {
            if (!obj.referencesClassExact()) {
                constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '" + obj + "'.");
            }
        } catch (final ClassNotFoundException e) {
            constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '" + obj + "'. which threw " + e);
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitNEWARRAY(final NEWARRAY o) {
        checkTypeIntConstraint(o, 0);
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitNOP(final NOP o) {
        // nothing is to be done here.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitPOP(final POP o) {
        if (stack().peek().getSize() != 1) {
            constraintViolated(o, "Stack top size should be 1 but stack top is '" + stack().peek() + "' of size '" + stack().peek().getSize() + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitPOP2(final POP2 o) {
        if (stack().peek().getSize() != 2) {
            constraintViolated(o, "Stack top size should be 2 but stack top is '" + stack().peek() + "' of size '" + stack().peek().getSize() + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitPUTFIELD(final PUTFIELD o) {
        try {

            final Type objectref = stack().peek(1);
            if (!(objectref instanceof ObjectType || objectref == Type.NULL)) {
                constraintViolated(o, "Stack next-to-top should be an object reference that's not an array reference, but is '" + objectref + "'.");
            }

            final Field f = visitFieldInstructionInternals(o);

            if (f.isProtected()) {
                final ObjectType classtype = getObjectType(o);
                final ObjectType curr = ObjectType.getInstance(mg.getClassName());

                if (classtype.equals(curr) || curr.subclassOf(classtype)) {
                    final Type tp = stack().peek(1);
                    if (tp == Type.NULL) {
                        return;
                    }
                    if (!(tp instanceof ObjectType)) {
                        constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '" + tp + "'.");
                    }
                    final ObjectType objreftype = (ObjectType) tp;
                    if (!(objreftype.equals(curr) || objreftype.subclassOf(curr))) {
                        constraintViolated(o,
                            "The referenced field has the ACC_PROTECTED modifier, and it's a member of the current class or"
                                + " a superclass of the current class. However, the referenced object type '" + stack().peek()
                                + "' is not the current class or a subclass of the current class.");
                    }
                }
            }

            // TODO: Could go into Pass 3a.
            if (f.isStatic()) {
                constraintViolated(o, "Referenced field '" + f + "' is static which it shouldn't be.");
            }

        } catch (final ClassNotFoundException e) {
            // FIXME: maybe not the best way to handle this
            throw new AssertionViolatedException("Missing class: " + e, e);
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitPUTSTATIC(final PUTSTATIC o) {
        try {
            visitFieldInstructionInternals(o);
        } catch (final ClassNotFoundException e) {
            // FIXME: maybe not the best way to handle this
            throw new AssertionViolatedException("Missing class: " + e, e);
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitRET(final RET o) {
        if (!(locals().get(o.getIndex()) instanceof ReturnaddressType)) {
            constraintViolated(o, "Expecting a ReturnaddressType in local variable " + o.getIndex() + ".");
        }
        if (locals().get(o.getIndex()) == ReturnaddressType.NO_TARGET) {
            throw new AssertionViolatedException("RET expecting a target.");
        }
        // Other constraints such as non-allowed overlapping subroutines are enforced
        // while building the Subroutines data structure.
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitRETURN(final RETURN o) {
        if (mg.getName().equals(Const.CONSTRUCTOR_NAME) && Frame.getThis() != null && !mg.getClassName().equals(Type.OBJECT.getClassName())) {
            constraintViolated(o, "Leaving a constructor that itself did not call a constructor.");
        }
    }

    /**
     * Assures the generic preconditions of a ReturnInstruction instance.
     */
    @Override
    public void visitReturnInstruction(final ReturnInstruction o) {
        Type methodType = mg.getType();
        if (methodType == Type.BOOLEAN || methodType == Type.BYTE || methodType == Type.SHORT || methodType == Type.CHAR) {
            methodType = Type.INT;
        }

        if (o instanceof RETURN) {
            if (methodType == Type.VOID) {
                return;
            }
            constraintViolated(o, "RETURN instruction in non-void method.");
        }
        if (o instanceof ARETURN) {
            if (methodType == Type.VOID) {
                constraintViolated(o, "ARETURN instruction in void method.");
            }
            if (stack().peek() == Type.NULL) {
                return;
            }
            if (!(stack().peek() instanceof ReferenceType)) {
                constraintViolated(o, "Reference type expected on top of stack, but is: '" + stack().peek() + "'.");
            }
            referenceTypeIsInitialized(o, (ReferenceType) stack().peek());
            // ReferenceType objectref = (ReferenceType) (stack().peek());
            // TODO: This can only be checked if using Staerk-et-al's "set of object types" instead of a
            // "wider cast object type" created during verification.
            // if (! (objectref.isAssignmentCompatibleWith(mg.getType())) ) {
            // constraintViolated(o, "Type on stack top which should be returned is a '"+stack().peek()+
            // "' which is not assignment compatible with the return type of this method, '"+mg.getType()+"'.");
            // }
        } else if (!methodType.equals(stack().peek())) {
            constraintViolated(o, "Current method has return type of '" + mg.getType() + "' expecting a '" + methodType
                + "' on top of the stack. But stack top is a '" + stack().peek() + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitSALOAD(final SALOAD o) {
        indexOfInt(o, stack().peek());
        checkArrayElementType(Type.SHORT, o, stack().peek(1));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitSASTORE(final SASTORE o) {
        checkTypeIntConstraint(o, 0);
        indexOfInt(o, stack().peek(1));
        checkArrayElementType(Type.SHORT, o, stack().peek(2));
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitSIPUSH(final SIPUSH o) {
        // nothing to do here. Generic visitXXX() methods did the trick before.
    }

    /**
     * Ensures the general preconditions of an instruction that accesses the stack. This method is here because BCEL has no
     * such superinterface for the stack accessing instructions; and there are funny unexpected exceptions in the semantices
     * of the superinterfaces and superclasses provided. E.g. SWAP is a StackConsumer, but DUP_X1 is not a StackProducer.
     * Therefore, this method is called by all StackProducer, StackConsumer, and StackInstruction instances via their
     * visitXXX() method. Unfortunately, as the superclasses and superinterfaces overlap, some instructions cause this
     * method to be called two or three times. [TODO: Fix this.]
     *
     * @see #visitStackConsumer(StackConsumer o)
     * @see #visitStackProducer(StackProducer o)
     * @see #visitStackInstruction(StackInstruction o)
     */
    private void visitStackAccessor(final Instruction o) {
        final int consume = o.consumeStack(cpg); // Stack values are always consumed first; then produced.
        if (consume > stack().slotsUsed()) {
            constraintViolated(o, "Cannot consume " + consume + " stack slots: only " + stack().slotsUsed() + " slot(s) left on stack!\nStack:\n" + stack());
        }

        final int produce = o.produceStack(cpg) - o.consumeStack(cpg); // Stack values are always consumed first; then produced.
        if (produce + stack().slotsUsed() > stack().maxStack()) {
            constraintViolated(o, "Cannot produce " + produce + " stack slots: only " + (stack().maxStack() - stack().slotsUsed())
                + " free stack slot(s) left.\nStack:\n" + stack());
        }
    }

    /**
     * Ensures the general preconditions of a StackConsumer instance.
     */
    @Override
    public void visitStackConsumer(final StackConsumer o) {
        visitStackAccessor((Instruction) o);
    }

    /**
     * Ensures the general preconditions of a StackInstruction instance.
     */
    @Override
    public void visitStackInstruction(final StackInstruction o) {
        visitStackAccessor(o);
    }

    /**
     * Ensures the general preconditions of a StackProducer instance.
     */
    @Override
    public void visitStackProducer(final StackProducer o) {
        visitStackAccessor((Instruction) o);
    }

    /**
     * Assures the generic preconditions of a StoreInstruction instance.
     */
    @Override
    public void visitStoreInstruction(final StoreInstruction o) {
        // visitLocalVariableInstruction(o) is called before, because it is more generic.

        if (stack().isEmpty()) { // Don't bother about 1 or 2 stack slots used. This check is implicitly done below while type checking.
            constraintViolated(o, "Cannot STORE: Stack to read from is empty.");
        }

        if (!(o instanceof ASTORE)) {
            if (!(stack().peek() == o.getType(cpg))) { // the other xSTORE types are singletons in BCEL.
                constraintViolated(o,
                    "Stack top type and STOREing Instruction type mismatch: Stack top: '" + stack().peek() + "'; Instruction type: '" + o.getType(cpg) + "'.");
            }
        } else { // we deal with ASTORE
            final Type stacktop = stack().peek();
            if (!(stacktop instanceof ReferenceType) && !(stacktop instanceof ReturnaddressType)) {
                constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '" + stack().peek()
                    + "'; Instruction expects a ReferenceType or a ReturnadressType.");
            }
            // if (stacktop instanceof ReferenceType) {
            // referenceTypeIsInitialized(o, (ReferenceType) stacktop);
            // }
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitSWAP(final SWAP o) {
        if (stack().peek().getSize() != 1) {
            constraintViolated(o, "The value at the stack top is not of size '1', but of size '" + stack().peek().getSize() + "'.");
        }
        if (stack().peek(1).getSize() != 1) {
            constraintViolated(o, "The value at the stack next-to-top is not of size '1', but of size '" + stack().peek(1).getSize() + "'.");
        }
    }

    /**
     * Ensures the specific preconditions of the said instruction.
     */
    @Override
    public void visitTABLESWITCH(final TABLESWITCH o) {
        indexOfInt(o, stack().peek());
        // See Pass 3a.
    }

}