fixes on GLB and returnloc calculation, etc.

[IRC.git] / Robust / src / ClassLibrary / SSJava / String.java

diff --git a/Robust/src/ClassLibrary/SSJava/String.java b/Robust/src/ClassLibrary/SSJava/String.java
index 4b061a82c6d8c107b6b69dc7ff41be72ea18cc61..b0abb612c8372b725642f1e513b9dd2b8d4e9cab 100644 (file)
--- a/Robust/src/ClassLibrary/SSJava/String.java
+++ b/Robust/src/ClassLibrary/SSJava/String.java
@@ -1,24 +1,33 @@
-@LATTICE("String_V<String_C, String_V<String_O")
-@METHODDEFAULT("StringDM_O<StringDM_V,StringDM_V<StringDM_C,StringDM_C<StringDM_I,THISLOC=StringDM_O,StringDM_C*")
+import Object;
+import String;
+
+@LATTICE("V<C, V<O")
+@METHODDEFAULT("O<V,V<C,C<IN,THISLOC=O,C*")
 public class String {
 
-  @LOC("String_V") char value[];
-  @LOC("String_C") int count;
-  @LOC("String_O") int offset;
-  @LOC("String_V") private int cachedHashcode;
+  @LOC("V") char value[];
+  @LOC("C") int count;
+  @LOC("O") int offset;
+  @LOC("V") private int cachedHashcode;
 
   private String() {
   }
+  
+  public String(String str) {
+    this.value=str.value;
+    this.count=str.count;
+    this.offset=str.offset;
+  }
 
-  public String(@LOC("StringDM_I") char c) {
-    @LOC("StringDM_V") char[] str = new char[1];
+  public String(@LOC("IN") char c) {
+    @LOC("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++)
+  public String(@LOC("IN") char str[]) {
+    @LOC("V") char charstr[]=new char[str.length];
+    for(@LOC("C") int i=0; i<str.length; i++)
       charstr[i]=str[i];
     this.value=charstr;
     charstr=null;
@@ -26,44 +35,66 @@ public class String {
     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;
+  @LATTICE("O<V,V<C,C<IN,THISLOC=IN,C*")
+  public String concat(@LOC("IN") String str) {
+    @LOC("O") String newstr=new String(); // create new one, it has OUT location
+    @LOC("C") int newCount=this.count+str.count;
 
-    @LOC("StringM1_V") char charstr[]=new char[newCount];
+    @LOC("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++) {
+    for(@LOC("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++) {
+    for(@LOC("C") int i=0; i<str.count; i++) {
       charstr[i+count]=str.value[i+str.offset];
     }
 
     newstr.value=charstr;
     charstr=null;
-    // LOC(newstr.value)=[O,STRING_V] 
+    // LOC(newstr.value)=[O,V] 
     // LOC(charstr)=[V]
-    // [O,STRING_V] < [V]
+    // [O,V] < [V]
     
     return newstr;
   }
   
-  public boolean equals(@LOC("StringDM_I") Object o) {
-    if (o.getType()!=getType()) // values are coming from [StringDM_I] and [THISLOC]
+  public boolean equals(@LOC("IN") Object o) {
+    if (o.getType()!=getType()) // values are coming from [IN] and [THISLOC]
       return false;
-    @LOC("StringDM_V") String s=(String)o;
+    @LOC("V") String s=(String)o;
     o=null;
     if (s.count!=count)
       return false;
-    for(@LOC("StringDM_C") int i=0; i<count; i++) {
+    for(@LOC("C") int i=0; i<count; i++) {
       if (s.value[i+s.offset]!=value[i+offset])
         return false;
     }
     return true;
   }
+  
+  @RETURNLOC("O")
+  public static String valueOf(@LOC("IN") Object o) {
+    if (o==null)
+      return "null";
+    else
+      return o.toString();
+  }
+  
+  public byte[] getBytes() {
+    byte str[]=new byte[count];
+    for(int i=0; i<count; i++)
+      str[i]=(byte)value[i+offset];
+    return str;
+  }
+
+  public int length() {
+    return count;
+  }
+  
+  public static native int convertdoubletochar(double val, char [] chararray);
+
 
 
 }