+
+ public String(@LOC("StringDM_I") char c) {
+ @LOC("StringDM_V") char[] str = new char[1];
+ str[0] = c;
+ String(str);
+ }
+
+ public String(@LOC("StringDM_I") char str[]) {
+ @LOC("StringDM_V") char charstr[]=new char[str.length];
+ for(@LOC("StringDM_C") int i=0; i<str.length; i++)
+ charstr[i]=str[i];
+ this.value=charstr;
+ this.count=str.length;
+ this.offset=0;
+ }
+
+ @LATTICE("StringM1_O<StringM1_V,StringM1_V<StringM1_C,StringM1_C<StringM1_I,THISLOC=StringM1_I,StringM1_C*")
+ public String concat(@LOC("StringM1_I") String str) {
+ @LOC("StringM1_O") String newstr=new String(); // create new one, it has OUT location
+ @LOC("StringM1_C") int newCount=this.count+str.count;
+
+ @LOC("StringM1_V") char charstr[]=new char[newCount];
+
+ // here, for loop introduces indirect flow from [C] to [V]
+ for(@LOC("StringM1_C") int i=0; i<count; i++) {
+ // value flows from GLB(THISLOC,C,THISLOC.V)=(THISLOC,TOP) to [V]
+ charstr[i]=value[i+offset];
+ }
+ for(@LOC("StringM1_C") int i=0; i<str.count; i++) {
+ charstr[i+count]=str.value[i+str.offset];
+ }
+
+ newstr.value=charstr;
+ // LOC(newstr.value)=[O,STRING_V]
+ // LOC(charstr)=[V]
+ // [O,STRING_V] < [V]
+
+ return newstr;
+ }