<NME> LongVecTest.java
<BEF> ADDFILE
<MSG> Add a range check to LongVec to prevent magically created
0/zero-elements. Such elements originate from an empty slot read (see
accompanying unit tests for scenarios).

<DFF> @@ -0,0 +1,142 @@
+/*******************************************************************************
+ * Copyright (c) 2015 Microsoft Research. All rights reserved. 
+ *
+ * The MIT License (MIT)
+ * 
+ * Permission is hereby granted, free of charge, to any person obtaining a copy 
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software. 
+ * 
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+
+package tlc2.util;
+
+import junit.framework.TestCase;
+
+public class LongVecTest extends TestCase {
+
+	protected LongVec getLongVec() {
+		// default capacity
+		return new LongVec();
+	}
+	
+	public void testReadBeyondCapacity() {
+		final LongVec vec = getLongVec();
+		try {
+			vec.elementAt(0);
+		} catch (IndexOutOfBoundsException e) {
+			return;
+		}
+		fail("Read beyond capacity");
+	}
+
+	public void testAddAndReadBeyondCapacity() {
+		final LongVec vec = getLongVec();
+		vec.addElement(1L);
+		assertEquals(1L, vec.elementAt(0));
+		try {
+			vec.elementAt(1);
+		} catch (IndexOutOfBoundsException e) {
+			return;
+		}
+		fail("Read beyond capacity");
+	}
+
+	public void testRemoveBeyondCapacity() {
+		final LongVec vec = new LongVec(10);
+		for (int i = -1; i <= 10; i++) {
+			try {
+				vec.removeElement(0);
+			} catch (IndexOutOfBoundsException e) {
+				continue;
+			}
+			fail("Read beyond capacity");
+		}
+	}
+
+	public void testAddRemoveBeyondCapacity() {
+		final LongVec vec = new LongVec(10);
+		vec.addElement(1L);
+		vec.removeElement(0);
+		try {
+			vec.removeElement(1);
+		} catch (IndexOutOfBoundsException e) {
+			return;
+		}
+		fail("Read beyond capacity");
+	}
+	
+	public void testRemoveAndGet() {
+		final LongVec vec = getLongVec();
+		vec.addElement(1L);
+		vec.addElement(2L);
+		vec.addElement(3L);
+		
+		assertEquals(1L, vec.elementAt(0));
+		assertEquals(2L, vec.elementAt(1));
+		assertEquals(3L, vec.elementAt(2));
+		
+		vec.removeElement(1);
+		assertEquals(1L, vec.elementAt(0));
+		assertEquals(3L, vec.elementAt(1));
+		// There must not be an element at idx 2 anymore!
+		try {
+			vec.elementAt(2);
+		} catch (IndexOutOfBoundsException e) {
+			return;
+		}
+		fail("A new elements magically appeared in LongVec");
+	}
+	
+	public void testRemoveWrongOrder() {
+		final LongVec vec = getLongVec();
+		vec.addElement(1L);
+		vec.addElement(2L);
+		
+		assertEquals(1L, vec.elementAt(0));
+		assertEquals(2L, vec.elementAt(1));
+		
+		vec.removeElement(0);
+		try {
+			vec.removeElement(1);
+		} catch (IndexOutOfBoundsException e) {
+			return;
+		}
+		fail("Removed non-existing element");
+	}
+
+	public void testGetNegative() {
+		final LongVec vec = getLongVec();
+		try {
+			vec.elementAt(-1);
+		} catch (IndexOutOfBoundsException e) {
+			return;
+		}
+		fail("Read negative");
+	}
+
+	public void testRemoveNegative() {
+		final LongVec vec = getLongVec();
+		try {
+			vec.removeElement(-1);
+		} catch (IndexOutOfBoundsException e) {
+			return;
+		}
+		fail("Removed negative");
+	}
+}

{'commit': 'diff --git a/tlatools/src/tlc2/util/LongVec.java b/tlatools/src/tlc2/util/LongVec.java\nindex b7b817197..f68364970 100644\n--- a/tlatools/src/tlc2/util/LongVec.java\n+++ b/tlatools/src/tlc2/util/LongVec.java\n@@ -10,101 +10,122 @@ import java.io.ObjectOutputStream;\n import java.io.Serializable;\n \n import util.FileUtil;\n+\n /**\n  * \n  * \n  * @version $Id$\n  */\n public class LongVec implements Cloneable, Serializable {\n-  private static final long serialVersionUID = 2406899362740899071L;\n-  protected long[] elementData;\n-  protected int elementCount;\n-         \n-  public LongVec() { this(10); }\n-\n-  public LongVec(int initialCapacity) {\n-    this.elementCount = 0;\n-    this.elementData = new long[initialCapacity];\n-  }\n-\n-  public final void addElement(long x) {\n-    if (this.elementCount == this.elementData.length) {\n-      ensureCapacity(this.elementCount+1);\n-    }\n-    this.elementData[this.elementCount++] = x;\n-  }\n-  \n-  public final long elementAt(int index) {\n-    return this.elementData[index];\n-  }\n-\n-  public final void removeElement(int index) {\n-    this.elementData[index] = this.elementData[this.elementCount-1];\n-    this.elementCount--;\n-  }\n-  \n-  public final int size() { return this.elementCount; }\n-  \n-  private final void ensureCapacity(int minCapacity) { \n-    if (elementData.length < minCapacity) {\n-      int newCapacity = elementData.length + elementData.length;\n-      if (newCapacity < minCapacity) {\n-\tnewCapacity = minCapacity;\n-      }\n-      long oldBuffer[] = this.elementData;\n-      this.elementData = new long[newCapacity];\n-\n-      System.arraycopy(oldBuffer, 0, elementData, 0, elementCount);\n-    }\n-  }\n+\tprivate static final long serialVersionUID = 2406899362740899071L;\n+\tprotected long[] elementData;\n+\tprotected int elementCount;\n \n-  public final void reset() { this.elementCount = 0; }\n+\tpublic LongVec() { this(10); }\n \n-  private void readObject(ObjectInputStream ois)\n-  throws IOException, ClassNotFoundException {\n-    this.elementCount = ois.readInt();\n-    this.elementData = new long[this.elementCount];\n-    for (int i = 0; i < this.elementCount; i++) {\n-      this.elementData[i] = ois.readLong();\n-    }\n-  }\n+\tpublic LongVec(int initialCapacity) {\n+\t\tthis.elementCount = 0;\n+\t\tthis.elementData = new long[initialCapacity];\n+\t}\n \n-  private void writeObject(ObjectOutputStream oos) throws IOException {\n-    oos.writeInt(this.elementCount);\n-    for (int i = 0; i < this.elementCount; i++) {\n-      oos.writeLong(this.elementData[i]);\n-    }\n-  }\n+\tpublic final void addElement(long x) {\n+\t\tif (this.elementCount == this.elementData.length) {\n+\t\t\tensureCapacity(this.elementCount + 1);\n+\t\t}\n+\t\tthis.elementData[this.elementCount++] = x;\n+\t}\n \n-  public final String toString() {\n-    StringBuffer sb = new StringBuffer();\n-    sb.append("<");\n-    if (this.elementCount != 0) {\n-      sb.append(this.elementData[0]);\n-    }\n-    for (int i = 1; i < this.elementCount; i++) {\n-      sb.append(", ");\n-      sb.append(this.elementData[i]);\n+\tpublic final long elementAt(int index) {\n+\t\trangeCheck(index);\n+\t\treturn this.elementData[index];\n+\t}\n+\n+\tpublic final void removeElement(int index) {\n+\t\trangeCheck(index);\n+\t\tthis.elementData[index] = this.elementData[this.elementCount - 1];\n+\t\tthis.elementCount--;\n+\t}\n+\n+\tprivate void rangeCheck(int index) {\n+\t\tif (index >= elementCount) {\n+\t\t\tthrow new IndexOutOfBoundsException(outOfBoundsMsg(index));\n+\t\t}\n+\t}\n+\t\n+    /**\n+     * Constructs an IndexOutOfBoundsException detail message.\n+     * Of the many possible refactorings of the error handling code,\n+     * this "outlining" performs best with both server and client VMs.\n+     */\n+\t// Copied from java.util.ArrayList\n+    private String outOfBoundsMsg(int index) {\n+        return "Index: "+index+", Size: "+elementCount;\n     }\n-    sb.append(">");\n-    return sb.toString();\n-  }\n-  \n-  public static void main(String args[]) throws Exception {\n-    LongVec vec = new LongVec(1000);\n-    vec.addElement(1);\n-    vec.addElement(3);\n-    vec.addElement(5);\n-    System.err.println(vec.size());\n-    ObjectOutputStream oos = FileUtil.newOBFOS("XXX");\n-    oos.writeObject(vec);\n-    \n-    ObjectInputStream ois = FileUtil.newOBFIS("XXX");\n-    LongVec vec1 = (LongVec)ois.readObject();\n-    System.err.println(vec1.size());\n-    System.err.println(vec1.elementAt(0));\n-    System.err.println(vec1.elementAt(1));\n-    System.err.println(vec1.elementAt(2));\n-  }\n+\n+\tpublic final int size() {\n+\t\treturn this.elementCount;\n+\t}\n+\n+\tprivate final void ensureCapacity(int minCapacity) {\n+\t\tif (elementData.length < minCapacity) {\n+\t\t\tint newCapacity = elementData.length + elementData.length;\n+\t\t\tif (newCapacity < minCapacity) {\n+\t\t\t\tnewCapacity = minCapacity;\n+\t\t\t}\n+\t\t\tlong oldBuffer[] = this.elementData;\n+\t\t\tthis.elementData = new long[newCapacity];\n+\n+\t\t\tSystem.arraycopy(oldBuffer, 0, elementData, 0, elementCount);\n+\t\t}\n+\t}\n+\n+\tpublic final void reset() { this.elementCount = 0; }\n+\n+\tprivate void readObject(ObjectInputStream ois)\n+\t\t\t  throws IOException, ClassNotFoundException {\n+\t\tthis.elementCount = ois.readInt();\n+\t\tthis.elementData = new long[this.elementCount];\n+\t\tfor (int i = 0; i < this.elementCount; i++) {\n+\t\t\tthis.elementData[i] = ois.readLong();\n+\t\t}\n+\t}\n+\n+\tprivate void writeObject(ObjectOutputStream oos) throws IOException {\n+\t\toos.writeInt(this.elementCount);\n+\t\tfor (int i = 0; i < this.elementCount; i++) {\n+\t\t\toos.writeLong(this.elementData[i]);\n+\t\t}\n+\t}\n+\n+\tpublic final String toString() {\n+\t\tStringBuffer sb = new StringBuffer();\n+\t\tsb.append("<");\n+\t\tif (this.elementCount != 0) {\n+\t\t\tsb.append(this.elementData[0]);\n+\t\t}\n+\t\tfor (int i = 1; i < this.elementCount; i++) {\n+\t\t\tsb.append(", ");\n+\t\t\tsb.append(this.elementData[i]);\n+\t\t}\n+\t\tsb.append(">");\n+\t\treturn sb.toString();\n+\t}\n+\n+\tpublic static void main(String args[]) throws Exception {\n+\t\tLongVec vec = new LongVec(1000);\n+\t\tvec.addElement(1);\n+\t\tvec.addElement(3);\n+\t\tvec.addElement(5);\n+\t\tSystem.err.println(vec.size());\n+\t\tObjectOutputStream oos = FileUtil.newOBFOS("XXX");\n+\t\toos.writeObject(vec);\n+\n+\t\tObjectInputStream ois = FileUtil.newOBFIS("XXX");\n+\t\tLongVec vec1 = (LongVec) ois.readObject();\n+\t\tSystem.err.println(vec1.size());\n+\t\tSystem.err.println(vec1.elementAt(0));\n+\t\tSystem.err.println(vec1.elementAt(1));\n+\t\tSystem.err.println(vec1.elementAt(2));\n+\t}\n \n }\ndiff --git a/tlatools/test/tlc2/util/GrowingLongVecTest.java b/tlatools/test/tlc2/util/GrowingLongVecTest.java\nnew file mode 100644\nindex 000000000..5d9d914ce\n--- /dev/null\n+++ b/tlatools/test/tlc2/util/GrowingLongVecTest.java\n@@ -0,0 +1,58 @@\n+/*******************************************************************************\r\n+ * Copyright (c) 2015 Microsoft Research. All rights reserved. \r\n+ *\r\n+ * The MIT License (MIT)\r\n+ * \r\n+ * Permission is hereby granted, free of charge, to any person obtaining a copy \r\n+ * of this software and associated documentation files (the "Software"), to deal\r\n+ * in the Software without restriction, including without limitation the rights\r\n+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies\r\n+ * of the Software, and to permit persons to whom the Software is furnished to do\r\n+ * so, subject to the following conditions:\r\n+ *\r\n+ * The above copyright notice and this permission notice shall be included in all\r\n+ * copies or substantial portions of the Software. \r\n+ * \r\n+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR\r\n+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS\r\n+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR\r\n+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN\r\n+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION\r\n+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.\r\n+ *\r\n+ * Contributors:\r\n+ *   Markus Alexander Kuppe - initial API and implementation\r\n+ ******************************************************************************/\r\n+\r\n+package tlc2.util;\r\n+\r\n+\r\n+public class GrowingLongVecTest extends LongVecTest {\r\n+\r\n+\t// A capacity that means the LongVec has to grow\r\n+\tprotected LongVec getLongVec() {\r\n+\t\treturn new LongVec(0);\r\n+\t}\r\n+\t\r\n+\tpublic void testGrowAndShrink() {\r\n+\t\t// Zero capacity, LongVec has to grow\r\n+\t\tfinal LongVec vec = new LongVec(0);\r\n+\t\tvec.addElement(1L);\r\n+\t\tvec.addElement(2L);\r\n+\r\n+\t\tassertEquals(2, vec.size());\r\n+\r\n+\t\t// Remove in reverse order\r\n+\t\tvec.removeElement(1);\r\n+\t\tvec.removeElement(0);\r\n+\t\t\r\n+\t\tassertEquals(0, vec.size());\r\n+\t\t\r\n+\t\ttry {\r\n+\t\t\tvec.removeElement(0);\r\n+\t\t} catch (Exception e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Removed non-existing element");\r\n+\t}\r\n+}\r\ndiff --git a/tlatools/test/tlc2/util/LongVecTest.java b/tlatools/test/tlc2/util/LongVecTest.java\nnew file mode 100644\nindex 000000000..2af02a8d0\n--- /dev/null\n+++ b/tlatools/test/tlc2/util/LongVecTest.java\n@@ -0,0 +1,142 @@\n+/*******************************************************************************\r\n+ * Copyright (c) 2015 Microsoft Research. All rights reserved. \r\n+ *\r\n+ * The MIT License (MIT)\r\n+ * \r\n+ * Permission is hereby granted, free of charge, to any person obtaining a copy \r\n+ * of this software and associated documentation files (the "Software"), to deal\r\n+ * in the Software without restriction, including without limitation the rights\r\n+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies\r\n+ * of the Software, and to permit persons to whom the Software is furnished to do\r\n+ * so, subject to the following conditions:\r\n+ *\r\n+ * The above copyright notice and this permission notice shall be included in all\r\n+ * copies or substantial portions of the Software. \r\n+ * \r\n+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR\r\n+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS\r\n+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR\r\n+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN\r\n+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION\r\n+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.\r\n+ *\r\n+ * Contributors:\r\n+ *   Markus Alexander Kuppe - initial API and implementation\r\n+ ******************************************************************************/\r\n+\r\n+package tlc2.util;\r\n+\r\n+import junit.framework.TestCase;\r\n+\r\n+public class LongVecTest extends TestCase {\r\n+\r\n+\tprotected LongVec getLongVec() {\r\n+\t\t// default capacity\r\n+\t\treturn new LongVec();\r\n+\t}\r\n+\t\r\n+\tpublic void testReadBeyondCapacity() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\ttry {\r\n+\t\t\tvec.elementAt(0);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Read beyond capacity");\r\n+\t}\r\n+\r\n+\tpublic void testAddAndReadBeyondCapacity() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\tvec.addElement(1L);\r\n+\t\tassertEquals(1L, vec.elementAt(0));\r\n+\t\ttry {\r\n+\t\t\tvec.elementAt(1);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Read beyond capacity");\r\n+\t}\r\n+\r\n+\tpublic void testRemoveBeyondCapacity() {\r\n+\t\tfinal LongVec vec = new LongVec(10);\r\n+\t\tfor (int i = -1; i <= 10; i++) {\r\n+\t\t\ttry {\r\n+\t\t\t\tvec.removeElement(0);\r\n+\t\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\t\tcontinue;\r\n+\t\t\t}\r\n+\t\t\tfail("Read beyond capacity");\r\n+\t\t}\r\n+\t}\r\n+\r\n+\tpublic void testAddRemoveBeyondCapacity() {\r\n+\t\tfinal LongVec vec = new LongVec(10);\r\n+\t\tvec.addElement(1L);\r\n+\t\tvec.removeElement(0);\r\n+\t\ttry {\r\n+\t\t\tvec.removeElement(1);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Read beyond capacity");\r\n+\t}\r\n+\t\r\n+\tpublic void testRemoveAndGet() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\tvec.addElement(1L);\r\n+\t\tvec.addElement(2L);\r\n+\t\tvec.addElement(3L);\r\n+\t\t\r\n+\t\tassertEquals(1L, vec.elementAt(0));\r\n+\t\tassertEquals(2L, vec.elementAt(1));\r\n+\t\tassertEquals(3L, vec.elementAt(2));\r\n+\t\t\r\n+\t\tvec.removeElement(1);\r\n+\t\tassertEquals(1L, vec.elementAt(0));\r\n+\t\tassertEquals(3L, vec.elementAt(1));\r\n+\t\t// There must not be an element at idx 2 anymore!\r\n+\t\ttry {\r\n+\t\t\tvec.elementAt(2);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("A new elements magically appeared in LongVec");\r\n+\t}\r\n+\t\r\n+\tpublic void testRemoveWrongOrder() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\tvec.addElement(1L);\r\n+\t\tvec.addElement(2L);\r\n+\t\t\r\n+\t\tassertEquals(1L, vec.elementAt(0));\r\n+\t\tassertEquals(2L, vec.elementAt(1));\r\n+\t\t\r\n+\t\tvec.removeElement(0);\r\n+\t\ttry {\r\n+\t\t\tvec.removeElement(1);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Removed non-existing element");\r\n+\t}\r\n+\r\n+\tpublic void testGetNegative() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\ttry {\r\n+\t\t\tvec.elementAt(-1);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Read negative");\r\n+\t}\r\n+\r\n+\tpublic void testRemoveNegative() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\ttry {\r\n+\t\t\tvec.removeElement(-1);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Removed negative");\r\n+\t}\r\n+}\r\n', 'commit_subject': 'Add a range check to LongVec to prevent magically created 0/zero-elements. Such elements originate from an empty slot read (see accompanying unit tests for scenarios).', 'repo_name': 'tlaplus/tlaplus', 'committer': {'name': 'Markus Alexander Kuppe', 'email': '82b77c4221e60124667659f5857eb35e1ec57936@lemmster.de', 'time_sec': '1427457027', 'tz_offset': '60', 'date': {'seconds': '1427457027'}}, 'commit_tree': '777c45610c21c32f6e5e529b61fa71cb41434ffb', 'commit_message': 'Add a range check to LongVec to prevent magically created\n0/zero-elements. Such elements originate from an empty slot read (see\naccompanying unit tests for scenarios).\n', 'language_name': 'R', 'license': 'mit', 'hunks': '@@ -0,0 +1,142 @@\n+/*******************************************************************************\r\n+ * Copyright (c) 2015 Microsoft Research. All rights reserved. \r\n+ *\r\n+ * The MIT License (MIT)\r\n+ * \r\n+ * Permission is hereby granted, free of charge, to any person obtaining a copy \r\n+ * of this software and associated documentation files (the "Software"), to deal\r\n+ * in the Software without restriction, including without limitation the rights\r\n+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies\r\n+ * of the Software, and to permit persons to whom the Software is furnished to do\r\n+ * so, subject to the following conditions:\r\n+ *\r\n+ * The above copyright notice and this permission notice shall be included in all\r\n+ * copies or substantial portions of the Software. \r\n+ * \r\n+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR\r\n+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS\r\n+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR\r\n+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN\r\n+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION\r\n+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.\r\n+ *\r\n+ * Contributors:\r\n+ *   Markus Alexander Kuppe - initial API and implementation\r\n+ ******************************************************************************/\r\n+\r\n+package tlc2.util;\r\n+\r\n+import junit.framework.TestCase;\r\n+\r\n+public class LongVecTest extends TestCase {\r\n+\r\n+\tprotected LongVec getLongVec() {\r\n+\t\t// default capacity\r\n+\t\treturn new LongVec();\r\n+\t}\r\n+\t\r\n+\tpublic void testReadBeyondCapacity() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\ttry {\r\n+\t\t\tvec.elementAt(0);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Read beyond capacity");\r\n+\t}\r\n+\r\n+\tpublic void testAddAndReadBeyondCapacity() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\tvec.addElement(1L);\r\n+\t\tassertEquals(1L, vec.elementAt(0));\r\n+\t\ttry {\r\n+\t\t\tvec.elementAt(1);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Read beyond capacity");\r\n+\t}\r\n+\r\n+\tpublic void testRemoveBeyondCapacity() {\r\n+\t\tfinal LongVec vec = new LongVec(10);\r\n+\t\tfor (int i = -1; i <= 10; i++) {\r\n+\t\t\ttry {\r\n+\t\t\t\tvec.removeElement(0);\r\n+\t\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\t\tcontinue;\r\n+\t\t\t}\r\n+\t\t\tfail("Read beyond capacity");\r\n+\t\t}\r\n+\t}\r\n+\r\n+\tpublic void testAddRemoveBeyondCapacity() {\r\n+\t\tfinal LongVec vec = new LongVec(10);\r\n+\t\tvec.addElement(1L);\r\n+\t\tvec.removeElement(0);\r\n+\t\ttry {\r\n+\t\t\tvec.removeElement(1);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Read beyond capacity");\r\n+\t}\r\n+\t\r\n+\tpublic void testRemoveAndGet() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\tvec.addElement(1L);\r\n+\t\tvec.addElement(2L);\r\n+\t\tvec.addElement(3L);\r\n+\t\t\r\n+\t\tassertEquals(1L, vec.elementAt(0));\r\n+\t\tassertEquals(2L, vec.elementAt(1));\r\n+\t\tassertEquals(3L, vec.elementAt(2));\r\n+\t\t\r\n+\t\tvec.removeElement(1);\r\n+\t\tassertEquals(1L, vec.elementAt(0));\r\n+\t\tassertEquals(3L, vec.elementAt(1));\r\n+\t\t// There must not be an element at idx 2 anymore!\r\n+\t\ttry {\r\n+\t\t\tvec.elementAt(2);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("A new elements magically appeared in LongVec");\r\n+\t}\r\n+\t\r\n+\tpublic void testRemoveWrongOrder() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\tvec.addElement(1L);\r\n+\t\tvec.addElement(2L);\r\n+\t\t\r\n+\t\tassertEquals(1L, vec.elementAt(0));\r\n+\t\tassertEquals(2L, vec.elementAt(1));\r\n+\t\t\r\n+\t\tvec.removeElement(0);\r\n+\t\ttry {\r\n+\t\t\tvec.removeElement(1);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Removed non-existing element");\r\n+\t}\r\n+\r\n+\tpublic void testGetNegative() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\ttry {\r\n+\t\t\tvec.elementAt(-1);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Read negative");\r\n+\t}\r\n+\r\n+\tpublic void testRemoveNegative() {\r\n+\t\tfinal LongVec vec = getLongVec();\r\n+\t\ttry {\r\n+\t\t\tvec.removeElement(-1);\r\n+\t\t} catch (IndexOutOfBoundsException e) {\r\n+\t\t\treturn;\r\n+\t\t}\r\n+\t\tfail("Removed negative");\r\n+\t}\r\n+}\r\n', 'addition_count': 142, 'deletion_count': 0, 'src_file': '/dev/null', 'tgt_file': 'b/tlatools/test/tlc2/util/LongVecTest.java', 'file_extension': '.java', 'before_file': 'ADDFILE', 'message': 'Add a range check to LongVec to prevent magically created\n0/zero-elements. Such elements originate from an empty slot read (see\naccompanying unit tests for scenarios).\n', 'author_name': 'Markus Alexander Kuppe', 'lang': 'java'}