src/peers/gov/nasa/jpf/vm/JPF_java_text_DateFormat.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18
  19 package gov.nasa.jpf.vm;
  20
  21 import gov.nasa.jpf.annotation.MJI;
  22 import gov.nasa.jpf.vm.MJIEnv;
  23 import gov.nasa.jpf.vm.NativePeer;
  24
  25 import java.text.DateFormat;
  26 import java.text.Format;
  27 import java.text.ParseException;
  28 import java.text.SimpleDateFormat;
  29 import java.util.Date;
  30 import java.util.TimeZone;
  31
  32 /**
  33  * this is just the minimal support for DateFormat.parse(String)
  34  */
  35 public class JPF_java_text_DateFormat extends NativePeer {
  36
  37   DateFormat getInstance (MJIEnv env, int objref) {
  38     Format fmt = JPF_java_text_Format.getInstance(env,objref);
  39     assert fmt instanceof SimpleDateFormat;
  40
  41     return (DateFormat)fmt;
  42   }
  43
  44   @MJI
  45   public void setTimeZone__Ljava_util_TimeZone_2__V(MJIEnv env, int objref,int timeZoneRef) {
  46     String timeZoneId = env.getStringField(timeZoneRef, "ID");
  47     TimeZone timeZone = TimeZone.getTimeZone(timeZoneId);
  48     DateFormat fmt = getInstance(env,objref);
  49     fmt.setTimeZone(timeZone);
  50     int calendarRef = env.getReferenceField(objref, "calendar");
  51     env.setReferenceField(calendarRef, "zone", timeZoneRef);
  52   }
  53
  54   @MJI
  55   public int parse__Ljava_lang_String_2__Ljava_util_Date_2 (MJIEnv env, int objref, int strRef) {
  56     DateFormat f = getInstance(env,objref);
  57     String s = env.getStringObject(strRef);
  58     try {
  59       Date d = f.parse(s);
  60       long t = d.getTime();
  61
  62       int dref = env.newObject("java.util.Date");
  63       env.setLongField(dref, "fastTime", t);
  64       return dref;
  65
  66     } catch (ClinitRequired x){
  67       env.handleClinitRequest(x.getRequiredClassInfo());
  68       return 0;
  69
  70     } catch (ParseException px) {
  71       env.throwException("java.text.ParseException", px.getMessage());
  72       return 0;
  73     }
  74   }
  75
  76   @MJI
  77   public void setLenient__Z__V (MJIEnv env, int objref, boolean isLenient) {
  78     DateFormat f = getInstance(env,objref);
  79     f.setLenient(isLenient);
  80   }
  81
  82   @MJI
  83   public int format__Ljava_util_Date_2__Ljava_lang_String_2 (MJIEnv env, int objref, int dateRef) {
  84     DateFormat fmt = getInstance(env,objref);
  85     if (fmt != null) {
  86       Date d = env.getDateObject(dateRef);
  87
  88       String s = fmt.format(d);
  89       int sref = env.newString(s);
  90       return sref;
  91     }
  92
  93     return MJIEnv.NULL;
  94   }
  95 }