Robust/src/ClassLibrary/SSJava/String.java

   1 @LATTICE("String_V<String_C, String_V<String_O")
   2 @METHODDEFAULT("StringDM_O<StringDM_V,StringDM_V<StringDM_C,StringDM_C<StringDM_I,THISLOC=StringDM_O,StringDM_C*")
   3 public class String {
   4
   5   @LOC("String_V") char value[];
   6   @LOC("String_C") int count;
   7   @LOC("String_O") int offset;
   8   @LOC("String_V") private int cachedHashcode;
   9
  10   private String() {
  11   }
  12
  13   public String(@LOC("StringDM_I") char c) {
  14     @LOC("StringDM_V") char[] str = new char[1];
  15     str[0] = c;
  16     String(str);
  17   }
  18
  19   public String(@LOC("StringDM_I") char str[]) {
  20     @LOC("StringDM_V") char charstr[]=new char[str.length];
  21     for(@LOC("StringDM_C") int i=0; i<str.length; i++)
  22       charstr[i]=str[i];
  23     this.value=charstr;
  24     this.count=str.length;
  25     this.offset=0;
  26   }
  27
  28   @LATTICE("StringM1_O<StringM1_V,StringM1_V<StringM1_C,StringM1_C<StringM1_I,THISLOC=StringM1_I,StringM1_C*")
  29   public String concat(@LOC("StringM1_I") String str) {
  30     @LOC("StringM1_O") String newstr=new String(); // create new one, it has OUT location
  31     @LOC("StringM1_C") int newCount=this.count+str.count;
  32
  33     @LOC("StringM1_V") char charstr[]=new char[newCount];
  34
  35     // here, for loop introduces indirect flow from [C] to [V]
  36     for(@LOC("StringM1_C") int i=0; i<count; i++) {
  37       // value flows from GLB(THISLOC,C,THISLOC.V)=(THISLOC,TOP) to [V]
  38       charstr[i]=value[i+offset];
  39     }
  40     for(@LOC("StringM1_C") int i=0; i<str.count; i++) {
  41       charstr[i+count]=str.value[i+str.offset];
  42     }
  43
  44     newstr.value=charstr;
  45     // LOC(newstr.value)=[O,STRING_V]
  46     // LOC(charstr)=[V]
  47     // [O,STRING_V] < [V]
  48
  49     return newstr;
  50   }
  51
  52   public boolean equals(@LOC("StringDM_I") Object o) {
  53     if (o.getType()!=getType()) // values are coming from [StringDM_I] and [THISLOC]
  54       return false;
  55     @LOC("StringDM_V") String s=(String)o;
  56     if (s.count!=count)
  57       return false;
  58     for(@LOC("StringDM_C") int i=0; i<count; i++) {
  59       if (s.value[i+s.offset]!=value[i+offset])
  60         return false;
  61     }
  62     return true;
  63   }
  64
  65
  66 }