From 6641f220c48a727f8811f95498af711372846b74 Mon Sep 17 00:00:00 2001 From: fresheed Date: Fri, 29 Mar 2019 15:56:57 +0300 Subject: [PATCH] Calendar peer bug demonstration (#181) * added unit test demonstrating Calendar peer bug * added comment and main() method which can be called by RunJPF utility --- .../nasa/jpf/test/java/util/CalendarTest.java | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 src/tests/gov/nasa/jpf/test/java/util/CalendarTest.java 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); + } + +} -- 2.34.1