Refactored the old testing class for records (#519)

* Refactored the old testing class for records and implemented separate classes for each test scenario. Some tests are expected to fail for now as full support for records is not yet implemented.

* Removed TODOs. we can add it later

Author: Mahmoud-Khawaja

src/tests/java17/RecordFeatureTest.java

@@ -0,0 +1,76 @@
+package java17.records;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+import java.lang.annotation.*;
+
+
+public class AnnotatedRecordTest extends TestJPF {
+
+    @Retention(RetentionPolicy.RUNTIME)
+    @Target({ElementType.TYPE, ElementType.RECORD_COMPONENT, ElementType.METHOD})
+    public @interface TestAnnotation {
+        String value() default "";
+    }
+
+    @Retention(RetentionPolicy.RUNTIME)
+    @Target({ElementType.RECORD_COMPONENT})
+    public @interface Field {
+        String name() default "";
+        boolean required() default false;
+    }
+
+    @TestAnnotation("Record class annotation")
+    record Person(
+            @Field(name = "firstName", required = true)
+            String firstName,
+
+            @Field(name = "lastName", required = true)
+            String lastName,
+
+            @Field(name = "age")
+            int age
+    ) {
+        @TestAnnotation("Custom method annotation")
+        public String fullName() {
+            return firstName + " " + lastName;
+        }
+    }
+
+    @Test
+    public void testRecordAnnotations() {
+        if (verifyNoPropertyViolation()) {
+            //class-level annotation
+            TestAnnotation classAnnotation = Person.class.getAnnotation(TestAnnotation.class);
+            assertNotNull(classAnnotation);
+            assertEquals("Record class annotation", classAnnotation.value());
+        }
+    }
+
+    @Test
+    public void testRecordMethodAnnotations() {
+        if (verifyNoPropertyViolation()) {
+            try {
+                java.lang.reflect.Method fullNameMethod = Person.class.getMethod("fullName");
+                TestAnnotation methodAnnotation = fullNameMethod.getAnnotation(TestAnnotation.class);
+                assertNotNull(methodAnnotation);
+                assertEquals("Custom method annotation", methodAnnotation.value());
+            } catch (Exception e) {
+                fail("Reflection on record method failed: " + e.getMessage());
+            }
+        }
+    }
+
+    @Test
+    public void testAnnotatedRecordBehavior() {
+        if (verifyNoPropertyViolation()) {
+            Person person = new Person("John", "Doe", 30);
+
+            // Basic functionality should still work
+            assertEquals("John", person.firstName());
+            assertEquals("Doe", person.lastName());
+            assertEquals(30, person.age());
+            assertEquals("John Doe", person.fullName());
+        }
+    }
+}

src/tests/java17/records/AnnotatedRecordTest.java

@@ -0,0 +1,106 @@
+package java17.records;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+
+public class BasicRecordTest extends TestJPF {
+
+    record Point(int x, int y) {}
+
+    record Temperature(double celsius) {
+        public Temperature {
+            if (celsius < -273.15) {
+                throw new IllegalArgumentException("Temperature below absolute zero");
+            }
+        }
+    }
+
+    record Rectangle(double width, double height) {
+        public double area() {
+            return width * height;
+        }
+
+        public double perimeter() {
+            return 2 * (width + height);
+        }
+    }
+
+    @Test
+    public void testRecordCreation() {
+        if (verifyNoPropertyViolation()) {
+            Point p = new Point(10, 20);
+            assertNotNull(p);
+        }
+    }
+
+    @Test
+    public void testRecordAccessors() {
+        if (verifyNoPropertyViolation()) {
+            Point p = new Point(10, 20);
+            // Test accessor methods
+            assertEquals(10, p.x());
+            assertEquals(20, p.y());
+        }
+    }
+
+    @Test
+    public void testRecordDirectFieldAccess() {
+        if (verifyNoPropertyViolation()) {
+            // This should NOT work if JPF properly enforces record encapsulation
+            // Field access should fail at compile time, but currently doesn't in JPF
+            Point p = new Point(10, 20);
+            try {
+                // using reflection to test access, as direct access would fail compilation in correct Java
+                java.lang.reflect.Field field = p.getClass().getDeclaredField("x");
+                field.setAccessible(true);
+                int value = (int) field.get(p);
+                assertEquals(10, value);
+
+                try {
+                    field.set(p, 30);
+                    fail("Should not be able to modify final field");
+                } catch (IllegalAccessException e) {
+                    // expected
+                }
+            } catch (Exception e) {
+                // expected if JPF correctly implements record field access -> will do later
+                assertTrue(e instanceof IllegalAccessException ||
+                        e instanceof NoSuchFieldException);
+            }
+        }
+    }
+
+    @Test
+    public void testRecordConstructorValidation() {
+        if (verifyNoPropertyViolation()) {
+            Temperature t1 = new Temperature(25.0);
+            assertEquals(25.0, t1.celsius(), 0.001);
+
+            // Invalid temperature (should throw exception)
+            try {
+                Temperature t2 = new Temperature(-300.0);
+                fail("Should have thrown IllegalArgumentException");
+            } catch (IllegalArgumentException e) {
+                // expected
+            }
+        }
+    }
+
+    @Test
+    public void testRecordCustomMethods() {
+        if (verifyNoPropertyViolation()) {
+            Rectangle r = new Rectangle(5.0, 10.0);
+            assertEquals(50.0, r.area(), 0.001);
+            assertEquals(30.0, r.perimeter(), 0.001);
+        }
+    }
+
+    @Test
+    public void testRecordToString() {
+        if (verifyNoPropertyViolation()) {
+            Point p = new Point(10, 20);
+            assertEquals("Point[x=10, y=20]", p.toString());
+        }
+    }
+}
+

src/tests/java17/records/BasicRecordTest.java

@@ -0,0 +1,84 @@
+package java17.records;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+import java.util.List;
+import java.util.ArrayList;
+import java.util.Arrays;
+
+public class GenericRecordTest extends TestJPF {
+
+    record Pair<T, U>(T first, U second) {}
+
+    record Box<T extends Comparable<T>>(T value) {
+        public boolean isGreaterThan(Box<T> other) {
+            return this.value.compareTo(other.value) > 0;
+        }
+    }
+
+    // record with collection type
+    record Collection<T>(List<T> items) {
+        public Collection<T> add(T item) {
+            List<T> newList = new ArrayList<>(items);
+            newList.add(item);
+            return new Collection<>(newList);
+        }
+
+        public int size() {
+            return items.size();
+        }
+    }
+
+    @Test
+    public void testGenericRecordCreation() {
+        if (verifyNoPropertyViolation()) {
+            Pair<String, Integer> p1 = new Pair<>("Hello", 42);
+            Pair<Double, Boolean> p2 = new Pair<>(3.14, true);
+
+            assertEquals("Hello", p1.first());
+            assertEquals(Integer.valueOf(42), p1.second());
+            assertEquals(Double.valueOf(3.14), p2.first());
+            assertEquals(Boolean.TRUE, p2.second());
+        }
+    }
+
+    @Test
+    public void testGenericRecordWithCollections() {
+        if (verifyNoPropertyViolation()) {
+            Collection<String> c1 = new Collection<>(new ArrayList<>());
+            Collection<String> c2 = c1.add("one").add("two").add("three");
+
+            assertEquals(0, c1.size());
+            assertEquals(3, c2.size());
+            assertEquals("one", c2.items().get(0));
+            assertEquals("two", c2.items().get(1));
+            assertEquals("three", c2.items().get(2));
+        }
+    }
+
+    @Test
+    public void testGenericRecordEquality() {
+        if (verifyNoPropertyViolation()) {
+            Pair<String, Integer> p1 = new Pair<>("Hello", 42);
+            Pair<String, Integer> p2 = new Pair<>("Hello", 42);
+            Pair<String, Integer> p3 = new Pair<>("Hello", 43);
+
+            assertEquals(p1, p2);
+            assertNotEquals(p1, p3);
+            assertEquals(p1.hashCode(), p2.hashCode());
+        }
+    }
+
+    @Test
+    public void testGenericRecordWithArrays() {
+        if (verifyNoPropertyViolation()) {
+            Pair<int[], String[]> arrayPair = new Pair<>(
+                    new int[]{1, 2, 3},
+                    new String[]{"a", "b", "c"}
+            );
+
+            assertTrue(Arrays.equals(new int[]{1, 2, 3}, arrayPair.first()));
+            assertTrue(Arrays.equals(new String[]{"a", "b", "c"}, arrayPair.second()));
+        }
+    }
+}