Add IndexOutOfBounds Tests

Author: rcosta358

liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/ArrayListRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.index_out_of_bounds_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+@Ghost("int size")
+public interface ArrayListRefinements<E> {
+
+    public void ArrayList();
+
+	@StateRefinement(to = "size(this) == size(old(this)) + 1")
+	public boolean add(E elem);
+
+	public E get(@Refinement("_ < size(this)") int index);
+}

liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_correct/Test.java

@@ -0,0 +1,11 @@
+package testSuite.classes.index_out_of_bounds_correct;
+
+import java.util.ArrayList;
+
+public class Test {
+    public static void main(String[] args) {
+        ArrayList<Integer> l = new ArrayList<>();
+        l.add(1);
+        l.get(0);
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/ArrayListRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.index_out_of_bounds_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+@Ghost("int size")
+public interface ArrayListRefinements<E> {
+
+    public void ArrayList();
+
+	@StateRefinement(to = "size(this) == size(old(this)) + 1")
+	public boolean add(E elem);
+
+	public E get(@Refinement("_ < size(this)") int index);
+}

liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/Test.java

@@ -0,0 +1,10 @@
+package testSuite.classes.index_out_of_bounds_error;
+
+import java.util.ArrayList;
+
+public class Test {
+    public static void main(String[] args) {
+        ArrayList<Integer> l = new ArrayList<>();
+        l.get(0); // index out of bounds
+    }
+}