From: yeom <yeom>
Date: Wed, 18 May 2011 01:34:57 +0000 (+0000)
Subject: updates ssjava test case to reflect recent changes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e5c82cd6c6fc85221b45acafd1a5d327f5fcaed0;p=IRC.git

updates ssjava test case to reflect recent changes
---

diff --git a/Robust/src/Tests/ssJava/flowdown/test.java b/Robust/src/Tests/ssJava/flowdown/test.java
index a2fd1362..fbcccc26 100644
--- a/Robust/src/Tests/ssJava/flowdown/test.java
+++ b/Robust/src/Tests/ssJava/flowdown/test.java
@@ -1,76 +1,62 @@
+@LATTICE("testL<testM,testM<testH")
+@METHODDEFAULT("methodL<methodH,methodH<methodT,THISLOC=methodT")
 public class test{
-    locdef{
-	F<D,F<E,D<B,E<C,B<A,C<A,A<T,T<U
-	//C<B,B<A,F<E,E<D,A<T,D<T
-    }
 
-    @A int a;
-    @B int b;
-    @C int c;
-    @D int d;
-    @E int e;
-    @T foo f;
-    @T bar bar;
-    @U foo u;
+    @LOC("testH") int fieldH;
+    @LOC("testM") int fieldM;
+    @LOC("testL") int fieldL;
+    @LOC("testM") Foo fooM;
 
-    public static void main (String args[]){
-	@T test t=new test();
+    public static void main (@LOC("methodH") String args[]){       
+	@LOC("methodH") test t=new test();
 	t.doit();
     }
 
     public void doit(){
-	//f=d+e;
-
-	@delta("LOC(d2result)") int d3result;
-	@delta("D,FC") int result;
-	@delta("LOC(result)") int d2result;
-
-	d3result=d2result+a;
-
-	//e=a+c;
-	
-	//result = f.a + f.b; // glb(f.a,f.b)=[T,FB]
-                            // then, compare LOC(result) and [T,FB]
+	@LOC("methodH") int localH; // LOC=[local.methodH]
+	fooM=new Foo(); // LOC=[local.methodT, field.testM]
+	fooM.doSomething();
 
-	//result=f.a+u.b;
+	// here, callee expects that arg1 is higher than arg2
+	// so caller should respects callee's constraints
+	fooM.doSomethingArgs(fieldH,fieldM);
 
-	//f.b=u.a; // u.a gives us a location: delta(U,FA)
-                 // f.b is at least lower than delta(U,FA)
-	         // by base comparison,
-                 // if LOC(f)<LOC(u) & LOC(foo.b)<LOC(foo.a)
-                 // then, it's okay
-
-	//bar.b=u.a; // u.a gives a new location: delta(U,FA)
-	           // bar.b is at least lower than delta(U,FA)
-                   // by base comparison
-                   // if LOC(bar)<LOC(u) 
-                   // but no ordering relation between LOC(bar.b) and LOC(foo.a)
-	           // is it okay to allow it?
-	           // seems to be okay because there is no way to
-	           // get it back to u.b or something else.	
+	doit2();
     }
-}
-
-class foo{
     
-    locdef{
-	FC<FB,FB<FA
+    public void doit2(){
+	@LOC("methodH,testL") int localVarL;
+	
+	// value flows from the field [local.methodH,field.testH]
+	// to the local variable [local.methodL]
+	localVarL=fieldH;
     }
-    
-    @FA int a;
-    @FB int b;
-    @FC int c;
-    
-}
 
-class bar{
+}
+@LATTICE("FC<FB,FB<FA")
+@METHODDEFAULT("fm_L<fm_M1,fm_L<fm_M2,fm_M1<fm_H,fm_M2<fm_H,THISLOC=fm_H")
+class Foo{
+	
+    @LOC("FA") int a;
+    @LOC("FB") int b;
+    @LOC("FC") int c;
+	
+    public Foo(){
+    }
 
-    locdef{
-	BC<BB,BB<BA
+    public void doSomething(){
+	b=a; // value flows from [fm_H,FA] to [fm_H,FB]
     }
 
-    @BA int a;
-    @BB int b;
-    @BC int c;
+    // callee has a constraint that arg1 is higher than arg2
+    public int doSomethingArgs(@LOC("fm_H")int argH,
+			       @LOC("fm_M1")int argL){	
+	argL=argH+50;
+	return argL;
+    }
 
+    public int doSomethingRtn(){
+	return a+b; // going to return LOC[local.t,field.FB]
+    }
+        
 }