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(@LOC("IN") String str) {
  17     this.value=str.value;
  18     this.count=str.count;
  19     this.offset=str.offset;
  20   }
  21
  22   public String(@LOC("IN") char c) {
  23     @LOC("V") char[] str = new char[1];
  24     str[0] = c;
  25     String(str);
  26   }
  27
  28   public String(@LOC("IN") char str[]) {
  29     @LOC("V") char charstr[]=new char[str.length];
  30     for(@LOC("C") int i=0; i<str.length; i++)
  31       charstr[i]=str[i];
  32     this.value=charstr;
  33     charstr=null;
  34     this.count=str.length;
  35     this.offset=0;
  36   }
  37
  38   @LATTICE("O<V,V<C,C<IN,THISLOC=IN,C*")
  39   @RETURNLOC("O")
  40   public String concat(@LOC("IN") String str) {
  41     @LOC("O") String newstr=new String(); // create new one, it has OUT location
  42     @LOC("C") int newCount=this.count+str.count;
  43
  44     @LOC("V") char charstr[]=new char[newCount];
  45
  46     // here, for loop introduces indirect flow from [C] to [V]
  47     for(@LOC("C") int i=0; i<count; i++) {
  48       // value flows from GLB(THISLOC,C,THISLOC.V)=(THISLOC,TOP) to [V]
  49       charstr[i]=value[i+offset];
  50     }
  51     for(@LOC("C") int i=0; i<str.count; i++) {
  52       charstr[i+count]=str.value[i+str.offset];
  53     }
  54
  55     newstr.value=charstr;
  56     charstr=null;
  57     // LOC(newstr.value)=[O,V]
  58     // LOC(charstr)=[V]
  59     // [O,V] < [V]
  60
  61     return newstr;
  62   }
  63
  64   @RETURNLOC("O")
  65   public boolean equals(@LOC("IN") Object o) {
  66     if (o.getType()!=getType()) // values are coming from [IN] and [THISLOC]
  67       return false;
  68     @LOC("V") String s=(String)o;
  69     o=null;
  70     if (s.count!=count)
  71       return false;
  72     for(@LOC("C") int i=0; i<count; i++) {
  73       if (s.value[i+s.offset]!=value[i+offset])
  74         return false;
  75     }
  76     return true;
  77   }
  78
  79   @RETURNLOC("O")
  80   public static String valueOf(@LOC("IN") Object o) {
  81     if (o==null)
  82       return "null";
  83     else
  84       return o.toString();
  85   }
  86
  87   @LATTICE("O<V,V<C,C<IN,THISLOC=IN,C*")
  88   @RETURNLOC("O")
  89   public byte[] getBytes() {
  90     @LOC("V") byte str[]=new byte[count];
  91     for(@LOC("C") int i=0; i<count; i++)
  92       str[i]=(byte)value[i+offset];
  93     return str;
  94   }
  95
  96   @RETURNLOC("IN")
  97   public int length() {
  98     return count;
  99   }
 100
 101   @RETURNLOC("O")
 102   public char charAt(@LOC("IN") int index){
 103     return value[index];
 104   }
 105
 106     //public static native int convertdoubletochar(double val, char [] chararray);
 107
 108 }