Calendar peer bug demonstration (#181)

* added unit test demonstrating Calendar peer bug

* added comment and main() method which can be called by RunJPF utility

diff --git a/src/tests/gov/nasa/jpf/test/java/util/CalendarTest.java b/src/tests/gov/nasa/jpf/test/java/util/CalendarTest.java
new file mode 100644 (file)
index 0000000..a4daf46
--- /dev/null
+++ b/src/tests/gov/nasa/jpf/test/java/util/CalendarTest.java
@@ -0,0 +1,36 @@
+package gov.nasa.jpf.test.java.util;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+
+import java.util.Calendar;
+
+// To reproduce bad behavior, run these tests on JPF VM: first should pass, second should fail
+// On HotSpot both tests pass
+public class CalendarTest extends TestJPF {
+
+    @Test
+    public void testCalendarHourSet(){
+        if (verifyNoPropertyViolation()){
+            Calendar cal = Calendar.getInstance();
+            cal.set(Calendar.HOUR_OF_DAY, 23);
+            assertEquals(23, cal.get(Calendar.HOUR_OF_DAY));
+        }
+    }
+
+    @Test
+    public void testCalendarHourSetAfterYear(){
+        if (verifyNoPropertyViolation()){
+            Calendar cal = Calendar.getInstance();
+            cal.set(Calendar.YEAR, 2014);
+            cal.set(Calendar.HOUR_OF_DAY, 23);
+            assertEquals(2014, cal.get(Calendar.YEAR));
+            assertEquals(23, cal.get(Calendar.HOUR_OF_DAY));
+        }
+    }
+
+    public static void main(String[] testMethods) {
+        runTestsOfThisClass(testMethods);
+    }
+
+}