src/tests/gov/nasa/jpf/test/java/util/CalendarTest.java

   1 package gov.nasa.jpf.test.java.util;
   2
   3 import gov.nasa.jpf.util.test.TestJPF;
   4 import org.junit.Test;
   5
   6 import java.util.Calendar;
   7
   8 // To reproduce bad behavior, run these tests on JPF VM: first should pass, second should fail
   9 // On HotSpot both tests pass
  10 public class CalendarTest extends TestJPF {
  11
  12     @Test
  13     public void testCalendarHourSet(){
  14         if (verifyNoPropertyViolation()){
  15             Calendar cal = Calendar.getInstance();
  16             cal.set(Calendar.HOUR_OF_DAY, 23);
  17             assertEquals(23, cal.get(Calendar.HOUR_OF_DAY));
  18         }
  19     }
  20
  21     @Test
  22     public void testCalendarHourSetAfterYear(){
  23         if (verifyNoPropertyViolation()){
  24             Calendar cal = Calendar.getInstance();
  25             cal.set(Calendar.YEAR, 2014);
  26             cal.set(Calendar.HOUR_OF_DAY, 23);
  27             assertEquals(2014, cal.get(Calendar.YEAR));
  28             assertEquals(23, cal.get(Calendar.HOUR_OF_DAY));
  29         }
  30     }
  31
  32     public static void main(String[] testMethods) {
  33         runTestsOfThisClass(testMethods);
  34     }
  35
  36 }