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