From: fresheed <ok.john.rus@gmail.com>
Date: Fri, 29 Mar 2019 12:56:57 +0000 (+0300)
Subject: Calendar peer bug demonstration (#181)
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=6641f220c48a727f8811f95498af711372846b74;ds=sidebyside

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
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);
+    }
+
+}