Robust/src/ClassLibrary/SSJava/String.java

   1 import Object;
   2 import String;
   3
   4 @LATTICE("V<C, V<O")
   5 @METHODDEFAULT("O<V,V<C,C<IN,THISLOC=O,C*")
   6 public class String {
   7
   8   @LOC("V") char value[];
   9   @LOC("C") int count;
  10   @LOC("O") int offset;
  11   @LOC("V") private int cachedHashcode;
  12
  13   private String() {
  14   }
  15
  16   public String(byte str[]) {
  17     char charstr[]=new char[str.length];
  18     for(int i=0; i<str.length; i++)
  19       charstr[i]=(char)str[i];
  20     this.value=charstr;
  21     this.count=str.length;
  22     this.offset=0;
  23   }
  24
  25
  26   public String(byte str[], String encoding) {
  27     int length = this.count;
  28     if (length>(str.length))
  29       length=str.length;
  30     char charstr[]=new char[length];
  31     for(int i=0; i<length; i++)
  32       charstr[i]=(char)str[i];
  33     this.value=charstr;
  34     this.count=length;
  35     this.offset=0;
  36   }
  37
  38   public String(@LOC("IN") String str) {
  39     this.value=str.value;
  40     this.count=str.count;
  41     this.offset=str.offset;
  42   }
  43
  44   public String(@LOC("IN") char c) {
  45     @LOC("V") char[] str = new char[1];
  46     str[0] = c;
  47     String(str);
  48   }
  49
  50   public String(@LOC("IN") char str[]) {
  51     @LOC("V") char charstr[]=new char[str.length];
  52     for(@LOC("C") int i=0; i<str.length; i++)
  53       charstr[i]=str[i];
  54     this.value=charstr;
  55     charstr=null;
  56     this.count=str.length;
  57     this.offset=0;
  58   }
  59
  60   @LATTICE("O<V,V<C,C<IN,THISLOC=IN,C*")
  61   @RETURNLOC("O")
  62   public String concat(@LOC("IN") String str) {
  63     @LOC("O") String newstr=new String(); // create new one, it has OUT location
  64     @LOC("C") int newCount=this.count+str.count;
  65
  66     @LOC("V") char charstr[]=new char[newCount];
  67
  68     // here, for loop introduces indirect flow from [C] to [V]
  69     for(@LOC("C") int i=0; i<count; i++) {
  70       // value flows from GLB(THISLOC,C,THISLOC.V)=(THISLOC,TOP) to [V]
  71       charstr[i]=value[i+offset];
  72     }
  73     for(@LOC("C") int i=0; i<str.count; i++) {
  74       charstr[i+count]=str.value[i+str.offset];
  75     }
  76
  77     newstr.value=charstr;
  78     charstr=null;
  79     // LOC(newstr.value)=[O,V]
  80     // LOC(charstr)=[V]
  81     // [O,V] < [V]
  82
  83     return newstr;
  84   }
  85
  86   @RETURNLOC("O")
  87   public boolean equals(@LOC("IN") Object o) {
  88     if (o.getType()!=getType()) // values are coming from [IN] and [THISLOC]
  89       return false;
  90     @LOC("V") String s=(String)o;
  91     o=null;
  92     if (s.count!=count)
  93       return false;
  94     for(@LOC("C") int i=0; i<count; i++) {
  95       if (s.value[i+s.offset]!=value[i+offset])
  96         return false;
  97     }
  98     return true;
  99   }
 100
 101   @RETURNLOC("O")
 102   public static String valueOf(@LOC("IN") Object o) {
 103     if (o==null)
 104       return "null";
 105     else
 106       return o.toString();
 107   }
 108
 109   public static String valueOf(boolean b) {
 110     if (b)
 111       return new String("true");
 112     else
 113       return new String("false");
 114   }
 115
 116   public static String valueOf(char c) {
 117     char ar[]=new char[1];
 118     ar[0]=c;
 119     return new String(ar);
 120   }
 121
 122   public static String valueOf(int x) {
 123     int length=0;
 124     int tmp;
 125     if (x<0)
 126       tmp=-x;
 127     else
 128       tmp=x;
 129     do {
 130       tmp=tmp/10;
 131       length=length+1;
 132     } while(tmp!=0);
 133
 134     char chararray[];
 135     if (x<0)
 136       chararray=new char[length+1];
 137     else
 138       chararray=new char[length];
 139     int voffset;
 140     if (x<0) {
 141       chararray[0]='-';
 142       voffset=1;
 143       x=-x;
 144     } else
 145       voffset=0;
 146
 147     do {
 148       chararray[--length+voffset]=(char)(x%10+'0');
 149       x=x/10;
 150     } while (length!=0);
 151     return new String(chararray);
 152   }
 153
 154   public static String valueOf(double val) {
 155     char[] chararray=new char[20];
 156     String s=new String();
 157     s.offset=0;
 158     s.count=convertdoubletochar(val, chararray);
 159     s.value=chararray;
 160     return s;
 161   }
 162
 163   public static String valueOf(long x) {
 164     int length=0;
 165     long tmp;
 166     if (x<0)
 167       tmp=-x;
 168     else
 169       tmp=x;
 170     do {
 171       tmp=tmp/10;
 172       length=length+1;
 173     } while(tmp!=0);
 174
 175     char chararray[];
 176     if (x<0)
 177       chararray=new char[length+1];
 178     else
 179       chararray=new char[length];
 180     int voffset;
 181     if (x<0) {
 182       chararray[0]='-';
 183       voffset=1;
 184       x=-x;
 185     } else
 186       voffset=0;
 187
 188     do {
 189       chararray[--length+voffset]=(char)(x%10+'0');
 190       x=x/10;
 191     } while (length!=0);
 192     return new String(chararray);
 193   }
 194
 195   @LATTICE("O<V,V<C,C<IN,THISLOC=IN,C*")
 196   @RETURNLOC("O")
 197   public byte[] getBytes() {
 198     @LOC("V") byte str[]=new byte[count];
 199     for(@LOC("C") int i=0; i<count; i++)
 200       str[i]=(byte)value[i+offset];
 201     return str;
 202   }
 203
 204
 205
 206   @RETURNLOC("IN")
 207   public int length() {
 208     return count;
 209   }
 210
 211   @RETURNLOC("O")
 212   public char charAt(@LOC("IN") int index){
 213     return value[index];
 214   }
 215
 216     //public static native int convertdoubletochar(double val, char [] chararray);
 217
 218 }