src/tests/gov/nasa/jpf/test/vm/basic/ExceptionHandlingTest.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.test.vm.basic;
  19
  20 import gov.nasa.jpf.util.test.TestJPF;
  21
  22 import java.lang.reflect.Method;
  23
  24 import org.junit.Test;
  25
  26 /**
  27  * JPF unit test for exception handling
  28  */
  29 @SuppressWarnings("null")
  30 public class ExceptionHandlingTest extends TestJPF {
  31   int data;
  32
  33   void foo () {
  34   }
  35
  36   static void bar () {
  37     ExceptionHandlingTest o = null;
  38     o.foo();
  39   }
  40
  41   @Test public void testNPE () {
  42     if (verifyUnhandledException("java.lang.NullPointerException")){
  43       ExceptionHandlingTest o = null;
  44       o.data = -1;
  45
  46       assert false : "should never get here";
  47     }
  48   }
  49
  50   @Test public void testNPECall () {
  51     if (verifyUnhandledException("java.lang.NullPointerException")){
  52       ExceptionHandlingTest o = null;
  53       o.foo();
  54
  55       assert false : "should never get here";
  56     }
  57   }
  58
  59   @Test public void testArrayIndexOutOfBoundsLow () {
  60     if (verifyUnhandledException("java.lang.ArrayIndexOutOfBoundsException")){
  61       int[] a = new int[10];
  62       a[-1] = 0;
  63
  64       assert false : "should never get here";
  65     }
  66   }
  67
  68   @Test public void testArrayIndexOutOfBoundsHigh () {
  69     if (verifyUnhandledException("java.lang.ArrayIndexOutOfBoundsException")){
  70       int[] a = new int[10];
  71       a[10] = 0;
  72
  73       assert false : "should never get here";
  74     }
  75   }
  76
  77   @Test public void testLocalHandler () {
  78     if (verifyNoPropertyViolation()){
  79       try {
  80         ExceptionHandlingTest o = null;
  81         o.data = 0;
  82       } catch (IllegalArgumentException iax) {
  83         assert false : "should never get here";
  84       } catch (NullPointerException npe) {
  85         return;
  86       } catch (Exception x) {
  87         assert false : "should never get here";
  88       }
  89
  90       assert false : "should never get here";
  91     }
  92   }
  93
  94   @Test public void testCallerHandler () {
  95     if (verifyNoPropertyViolation()){
  96       try {
  97         bar();
  98       } catch (Throwable t) {
  99         return;
 100       }
 101
 102       assert false : "should never get here";
 103     }
 104   }
 105
 106   @Test public void testEmptyHandler () {
 107     if (verifyNoPropertyViolation()){
 108       try {
 109         throw new RuntimeException("should be empty-handled");
 110       } catch (Throwable t) {
 111         // nothing
 112       }
 113     }
 114   }
 115
 116   @Test public void testEmptyTryBlock () {
 117     if (verifyNoPropertyViolation()){
 118       try {
 119         // nothing
 120       } catch (Throwable t) {
 121         assert false : "should never get here";
 122       }
 123     }
 124   }
 125
 126   @Test public void testStackTrace() {
 127     if (verifyNoPropertyViolation()){
 128
 129       Throwable x = new Throwable();
 130       StackTraceElement[] st = x.getStackTrace();
 131
 132       //x.printStackTrace();
 133       for (int i=0; i<st.length; i++){
 134         System.out.print("\t at ");
 135         System.out.print(st[i].getClassName());
 136         System.out.print('.');
 137         System.out.print(st[i].getMethodName());
 138         System.out.print('(');
 139         System.out.print(st[i].getFileName());
 140         System.out.print(':');
 141         System.out.print(st[i].getLineNumber());
 142         System.out.println(')');
 143       }
 144
 145       // note - direct call stackframes should not show up here, they are JPF internal
 146       assert st.length == 3 : "wrong stack trace depth";
 147
 148       assert st[0].getClassName().equals(ExceptionHandlingTest.class.getName());
 149       assert st[0].getMethodName().equals("testStackTrace");
 150
 151       assert st[1].getClassName().equals(Method.class.getName());
 152       assert st[1].getMethodName().equals("invoke");
 153
 154       assert st[2].getClassName().equals(TestJPF.class.getName());
 155       assert st[2].getMethodName().equals("runTestMethod");
 156     }
 157   }
 158 }
 159