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 5eb9135f6a90bfebccfcc211c6f21b76c26a5cbb..eda4afd88b6f950e40b262b0ba7e85c7973e3c92 100644 (file)
--- 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 fbcccc26ff5b9c784150b91990be9ec46f46761c..f17f3f5b5b26f60fe642e75e84003d1f94ab405a 100644 (file)
--- 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{