From: yeom <yeom>
Date: Wed, 18 May 2011 18:59:14 +0000 (+0000)
Subject: add more test cases: delta func and local variable lattice
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=2f9ab427cc817bcd05c2b0ee43c2c5cf6e9e9f89;p=IRC.git

add more test cases: delta func and local variable lattice
---

diff --git a/Robust/src/Tests/ssJava/flowdown/makefile b/Robust/src/Tests/ssJava/flowdown/makefile
index 5eb9135f..eda4afd8 100644
--- a/Robust/src/Tests/ssJava/flowdown/makefile
+++ b/Robust/src/Tests/ssJava/flowdown/makefile
@@ -8,7 +8,7 @@ BSFLAGS= -32bit -ssjava -printlinenum -mainclass $(PROGRAM)  -heapsize-mb 1000 -
 default: $(PROGRAM)s.bin
 
 $(PROGRAM)s.bin: $(SOURCE_FILES) makefile
-	$(BUILDSCRIPT) -thread $(BSFLAGS) -o $(PROGRAM)s -builddir sing $(SOURCE_FILES) 
+	$(BUILDSCRIPT) $(BSFLAGS) -o $(PROGRAM)s -builddir sing $(SOURCE_FILES) 
 
 clean:
 	rm -f  $(PROGRAM)s.bin
diff --git a/Robust/src/Tests/ssJava/flowdown/test.java b/Robust/src/Tests/ssJava/flowdown/test.java
index fbcccc26..f17f3f5b 100644
--- a/Robust/src/Tests/ssJava/flowdown/test.java
+++ b/Robust/src/Tests/ssJava/flowdown/test.java
@@ -22,6 +22,8 @@ public class test{
 	fooM.doSomethingArgs(fieldH,fieldM);
 
 	doit2();
+	doOwnLattice();
+	doDelta();
     }
     
     public void doit2(){
@@ -32,7 +34,32 @@ public class test{
 	localVarL=fieldH;
     }
 
+    // method has its own local variable lattice 
+    @LATTICE("mL<mH,THISLOC=mH")
+    public void doOwnLattice(){
+	@LOC("mL") int varL;
+	@LOC("mH") int varH;
+	varL=varH;
+    }
+    
+      
+    @LATTICE("mL<mH,THISLOC=mH")
+    public void doDelta(){
+	@LOC("DELTA(mH,testH)") int varDelta;
+	// LOC(varDelta) is slightly lower than [mH, testH]
+
+	@LOC("DELTA(DELTA(mH,testH))") int varDeltax2;
+	// applying double delta to [mH,testH]
+	
+	varDelta=fieldH; // [mH,testH] -> DELTA[mh,testH]
+	varDeltax2=varDelta; //DELTA[mh,testH] -> DELTA[DELTA[mh,testH]]
+	
+	fieldM=varDeltax2; //  DELTA[DELTA[mh,testH]] -> [mH,testM]	
+    }
+
 }
+
+
 @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{