Added tests, one failing and one correct

Author: Antonio Almeida

latte/src/test/examples/LinkedListRefinement.java

@@ -0,0 +1,27 @@
+import specification.*;
+import java.util.LinkedList;
+
+public class LinkedListRefinement {
+    @Unique Object o1;
+
+    public Object test(Object obj, Object obj2, @Free Object temp) {
+        LinkedList<Object> list = new LinkedList<>();
+
+        list.add(obj);
+        list.add(obj);
+        list.add(1, obj2);
+
+        list.remove(temp);
+    }
+}
+
+@ExternalRefinementsFor("java.util.LinkedList")
+interface LinkedListRefinements2<T> {
+
+    public void add(@Shared T t);
+
+    public void add(int n, @Shared T t);
+
+    public void remove(@Free T t);
+
+}

latte/src/test/examples/LinkedListRefinementIncorrect.java

@@ -0,0 +1,24 @@
+import specification.*;
+import java.util.LinkedList;
+
+public class LinkedListRefinementIncorrect {
+    @Unique Object o1;
+
+    public Object test(@Free Object obj) {
+        Object o2 = o1;
+        LinkedList<Object> list = new LinkedList<>();
+
+        list.add(obj);
+        list.add(o2);
+    }
+}
+
+@ExternalRefinementsFor("java.util.LinkedList")
+interface LinkedListRefinements<T> {
+
+    public void add(@Free T t);
+
+    public void add(int n, T t);
+
+    public void remove(@Free T t);
+}

latte/src/test/java/AppTest.java

@@ -40,7 +40,8 @@ private static Stream<Arguments> provideCorrectTestCases() {
             Arguments.of("src/test/examples/searching_state_space/TimerTaskCannotReschedule.java"),
             Arguments.of("src/test/examples/searching_state_space/ResultSetNoNext.java"),
             Arguments.of("src/test/examples/searching_state_space/ResultSetForwardOnly.java"),
-            Arguments.of("src/test/examples/stack_overflow/MediaRecord.java")
+            Arguments.of("src/test/examples/stack_overflow/MediaRecord.java"),
+            Arguments.of("src/test/examples/LinkedListRefinement.java")
         );
     }
 
@@ -60,7 +61,8 @@ private static Stream<Arguments> provideIncorrectTestCases() {
             Arguments.of("src/test/examples/SmallestIncorrectExample.java", "UNIQUE but got BORROWED"),
             Arguments.of("src/test/examples/MyStackFieldAssignMethod.java", "UNIQUE but got SHARED"),
             Arguments.of("src/test/examples/FieldAccessNoThis.java", "UNIQUE but got SHARED"),
-            Arguments.of("src/test/examples/FieldAccessRightNoThis.java", "FREE but got UNIQUE")
+            Arguments.of("src/test/examples/FieldAccessRightNoThis.java", "FREE but got UNIQUE"),
+                Arguments.of("src/test/examples/LinkedListRefinementIncorrect.java", "FREE but got UNIQUE")
         );
     }