From 061a6733a671ae5a8a42d4d238e05aede5656b82 Mon Sep 17 00:00:00 2001
From: yeom <yeom>
Date: Fri, 16 Dec 2011 19:58:12 +0000
Subject: [PATCH] test case for the ownership checking

---
 Robust/src/Tests/ssJava/ownership/makefile  | 26 ++++++
 Robust/src/Tests/ssJava/ownership/test.java | 87 +++++++++++++++++++++
 2 files changed, 113 insertions(+)
 create mode 100644 Robust/src/Tests/ssJava/ownership/makefile
 create mode 100644 Robust/src/Tests/ssJava/ownership/test.java

diff --git a/Robust/src/Tests/ssJava/ownership/makefile b/Robust/src/Tests/ssJava/ownership/makefile
new file mode 100644
index 00000000..b6d1119d
--- /dev/null
+++ b/Robust/src/Tests/ssJava/ownership/makefile
@@ -0,0 +1,26 @@
+BUILDSCRIPT=../../../buildscript
+
+PROGRAM=test
+SOURCE_FILES=test.java
+
+BSFLAGS= -32bit -ssjava -ssjavadebug -printlinenum -mainclass $(PROGRAM)  -heapsize-mb 1000 -garbagestats -joptimize -optimize -debug #-nooptimize #src-after-pp #-debug
+
+default: $(PROGRAM)s.bin
+
+$(PROGRAM)s.bin: $(SOURCE_FILES) makefile
+	$(BUILDSCRIPT) $(BSFLAGS) -o $(PROGRAM)s -builddir sing $(SOURCE_FILES) 
+
+clean:
+	rm -f  $(PROGRAM)s.bin
+	rm -fr sing
+	rm -f tmp.c
+	rm -f  *~
+	rm -f  *.dot
+	rm -f  *.png
+	rm -f  *.txt
+	rm -f  aliases.txt
+	rm -f  mlpReport*txt
+	rm -f  results*txt
+	rm -f *log
+	rm -f coreprof.dat
+	rm -f trace.out
diff --git a/Robust/src/Tests/ssJava/ownership/test.java b/Robust/src/Tests/ssJava/ownership/test.java
new file mode 100644
index 00000000..37811077
--- /dev/null
+++ b/Robust/src/Tests/ssJava/ownership/test.java
@@ -0,0 +1,87 @@
+@LATTICE("L<M,M<H,H<C,C*,M*")
+@METHODDEFAULT("L<M,M<H,H<IN,THISLOC=M,RETURNLOC=M")
+public class test {
+
+  @LOC("H")
+  Foo foo;
+  @LOC("H")
+  Foo f1;
+
+  public static void main(@LOC("H") String args[]) {
+    @LOC("H") test t = new test();
+
+    SSJAVA: while (true) {
+      t.doDelegationTest();
+      t.doDelegationTest2();
+    }
+
+  }
+
+  public void doDelegationTest() {
+
+    @LOC("H") Foo ownedFoo = new Foo();
+    delegate(ownedFoo);
+    // ERROR::
+    // System.out.println(ownedFoo.v);
+
+    changeLocationTest(ownedFoo);
+  }
+
+  public void delegate(@DELEGATE @LOC("IN") Foo foo) {
+    @LOC("M") Foo lowerFoo = foo; // allowed to lower
+
+    // create a temp var to walk the subtree
+    @LOC("L") Bar tempVar = lowerFoo.bar1;
+    lowerFoo.bar1 = null;
+
+  }
+
+  public void changeLocationTest(@DELEGATE @LOC("IN") Foo foo) {
+
+    // local variable refers to the sub object the foo
+    @LOC("M") Bar tempVar = foo.bar1;
+
+    // ERROR: not allowed to lower if there is a local var alias to the subtree
+    // of the foo
+    // @LOC("M") Foo lowerFoo = foo;
+
+  }
+
+  public void doDelegationTest2() {
+
+    @LOC("H") Foo ownedFoo = new Foo();
+    notDelegate(ownedFoo);
+
+  }
+
+  public Foo notDelegate(@LOC("IN") Foo notownedFoo) {
+
+    // ERROR: not allowed to lower
+    // @LOC("M") Foo lowerFoo = notownedFoo;
+
+    // ERROR: now allowed to return not-owned-ref
+    return notownedFoo;
+
+  }
+
+}
+
+@LATTICE("L<M,M<H,H<C,C*,M*")
+@METHODDEFAULT("T")
+class Foo {
+  @LOC("H")
+  Bar bar1;
+  @LOC("H")
+  Bar bar2;
+  @LOC("H")
+  int v;
+}
+
+@LATTICE("L<M,M<H,H<C,C*,M*")
+@METHODDEFAULT("T")
+class Bar {
+  @LOC("M")
+  int v1;
+  @LOC("M")
+  int v2;
+}
-- 
2.34.1