src/tests/gov/nasa/jpf/test/vm/basic/ArrayTest.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 org.junit.Test;
  23
  24 /**
  25  * JPF part of unit test for standard VM array operations.
  26  */
  27 public class ArrayTest extends TestJPF {
  28
  29   @Test
  30   public void test2DArray() {
  31     if (verifyNoPropertyViolation()) {
  32       long[][] a = new long[2][3];
  33
  34       a[0][1] = 42;
  35
  36       assert (a.getClass().isArray());
  37       assert (a.getClass().getName().equals("[[J"));
  38       assert (a.getClass().getComponentType().getName().equals("[J"));
  39       assert (a[0][1] == 42);
  40     }
  41   }
  42
  43   @Test
  44   public void test2DStringArray() {
  45     if (verifyNoPropertyViolation()) {
  46       String[][] a = new String[3][5];
  47
  48       a[2][2] = "fortytwo";
  49
  50       assert (a.getClass().isArray());
  51       assert (a.getClass().getName().equals("[[Ljava.lang.String;"));
  52       assert (a.getClass().getComponentType().getName().equals("[Ljava.lang.String;"));
  53       assert (a[2][2].equals("fortytwo"));
  54     }
  55   }
  56
  57   @Test
  58   public void testAoBX() {
  59     if (verifyNoPropertyViolation()) {
  60       int[] a = new int[2];
  61
  62       assert (a.length == 2);
  63
  64       try {
  65         a[2] = 42;
  66       } catch (ArrayIndexOutOfBoundsException aobx) {
  67         return;
  68       }
  69
  70       throw new RuntimeException("array bounds check failed (no ArrayIndexOutOfBoundsException)");
  71     }
  72   }
  73
  74   @Test
  75   public void testArrayStoreException() {
  76     if (verifyNoPropertyViolation()) {
  77       try {
  78         Object x[] = new String[1];
  79         x[0] = new Integer(42);
  80       } catch (ArrayStoreException osx) {
  81         return;
  82       }
  83
  84       throw new RuntimeException("array element type check failed (no ArrayStoreException)");
  85     }
  86   }
  87
  88   @Test
  89   public void testArrayStoreExceptionArraycopy() {
  90     if (verifyNoPropertyViolation()) {
  91
  92       boolean caught = false;
  93       try {
  94         System.arraycopy(new Object[]{new Integer(42)}, 0, new String[2], 0, 1);
  95       } catch (ArrayStoreException x) {
  96         caught = true;
  97       }
  98       if (!caught) {
  99         throw new RuntimeException("array element type check failed (no ArrayStoreException: Integer[] -> String[])");
 100       }
 101
 102       caught = false;
 103       try {
 104         System.arraycopy(new Object[]{new Integer(42)}, 0, new int[2], 0, 1);
 105       } catch (ArrayStoreException x) {
 106         caught = true;
 107       }
 108       if (!caught) {
 109         throw new RuntimeException("array element type check failed (no ArrayStoreException: Integer[] -> int[])");
 110       }
 111
 112       caught = false;
 113       try {
 114         System.arraycopy(new int[]{42, 42}, 0, new long[2], 0, 1);
 115       } catch (ArrayStoreException x) {
 116         caught = true;
 117       }
 118       if (!caught) {
 119         throw new RuntimeException("array element type check failed (no ArrayStoreException: int[] -> long[])");
 120       }
 121
 122       caught = false;
 123       try {
 124         System.arraycopy(new int[]{42, 42}, 0, new float[2], 0, 1);
 125       } catch (ArrayStoreException x) {
 126         caught = true;
 127       }
 128       if (!caught) {
 129         throw new RuntimeException("array element type check failed (no ArrayStoreException: int[] -> float[])");
 130       }
 131
 132       caught = false;
 133       try {
 134         System.arraycopy(new double[]{42, 42}, 0, new long[2], 0, 1);
 135       } catch (ArrayStoreException x) {
 136         caught = true;
 137       }
 138       if (!caught) {
 139         throw new RuntimeException("array element type check failed (no ArrayStoreException: double[] -> long[])");
 140       }
 141     }
 142   }
 143
 144   @Test
 145   public void testCharArray() {
 146     if (verifyNoPropertyViolation()) {
 147
 148       char[] a = new char[5];
 149
 150       a[2] = 'Z';
 151
 152       assert (a.getClass().isArray());
 153       assert (a.getClass().getName().equals("[C"));
 154       assert (a.getClass().getComponentType() == char.class);
 155       assert (a[2] == 'Z');
 156     }
 157   }
 158
 159   @Test
 160   public void testIntArray() {
 161     if (verifyNoPropertyViolation()) {
 162
 163       int[] a = new int[10];
 164
 165       a[1] = 42;
 166
 167       assert (a.getClass().isArray());
 168       assert (a.getClass().getName().equals("[I"));
 169       assert (a.getClass().getComponentType() == int.class);
 170       assert (a[1] == 42);
 171     }
 172   }
 173
 174   @Test
 175   public void testStringArray() {
 176     if (verifyNoPropertyViolation()) {
 177
 178       String[] a = {"one", "two", "three"};
 179
 180       assert (a.getClass().isArray());
 181       assert (a.getClass().getName().equals("[Ljava.lang.String;"));
 182       assert (a.getClass().getComponentType() == String.class);
 183       assert (a[1].equals("two"));
 184     }
 185   }
 186
 187   @Test
 188   public void testArrayCopy() {
 189     if (verifyNoPropertyViolation()) {
 190
 191       String s1 = "1";
 192       String s2 = "2";
 193       String s3 = "3";
 194       String[] sa = {s1, s2, s3};
 195       String[] sb = {s3, s2, s1};
 196
 197       System.arraycopy(sa, 0, sb, 1, 2);
 198       assert (sb[0] == s3 && sb[1] == s1 && sb[2] == s2);
 199
 200       System.arraycopy(sa, 0, sa, 1, 2);
 201       assert (sa[0] == s1 && sa[1] == s1 && sa[2] == s2);
 202
 203       System.arraycopy(sb, 1, sb, 0, 2);
 204       assert (sb[0] == s1 && sb[1] == s2 && sb[2] == s2);
 205
 206       System.arraycopy(sa, 3, sb, 0, 0);
 207       assert (sb[0] == s1 && sb[1] == s2 && sb[2] == s2);
 208
 209
 210       long[] la = {1L, 2L, 3L};
 211       long[] lb = {3L, 2L, 1L};
 212
 213       System.arraycopy(la, 0, lb, 1, 2);
 214       assert (lb[0] == 3 && lb[1] == 1 && lb[2] == 2);
 215
 216       System.arraycopy(la, 0, la, 1, 2);
 217       assert (la[0] == 1 && la[1] == 1 && la[2] == 2);
 218
 219       System.arraycopy(lb, 1, lb, 0, 2);
 220       assert (lb[0] == 1 && lb[1] == 2 && lb[2] == 2);
 221
 222       System.arraycopy(la, 3, lb, 0, 0);
 223       assert (lb[0] == 1 && lb[1] == 2 && lb[2] == 2);
 224     }
 225   }
 226 }