added tests

10 files changed, 258 insertions, 0 deletions

diff --git a/Test/og/Program1.bpl b/Test/og/Program1.bpl
new file mode 100644
index 00000000..56620da2
--- /dev/null
+++ b/Test/og/Program1.bpl
@@ -0,0 +1,29 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+var {:phase 1} x:int;

+

+procedure {:yields} {:phase 1} p() 

+requires {:phase 1} x >= 5; 

+ensures {:phase 1} x >= 8; 

+{ 

+    yield;

+    assert {:phase 1} x >= 5; 

+    call Incr(1); 

+    yield;

+    assert {:phase 1} x >= 6; 

+    call Incr(1); 

+    yield;

+    assert {:phase 1} x >= 7;

+    call Incr(1); 

+}

+

+procedure {:yields} {:phase 1} q() 

+{ 

+    call Incr(3); 

+}

+

+procedure {:yields} {:phase 0,1} Incr(val: int);

+ensures {:atomic}

+|{A:

+  x := x + val; return true;

+}|;

diff --git a/Test/og/Program1.bpl.expect b/Test/og/Program1.bpl.expect
new file mode 100644
index 00000000..3de74d3e
--- /dev/null
+++ b/Test/og/Program1.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 2 verified, 0 errors

diff --git a/Test/og/Program2.bpl b/Test/og/Program2.bpl
new file mode 100644
index 00000000..7713a5d2
--- /dev/null
+++ b/Test/og/Program2.bpl
@@ -0,0 +1,34 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+var {:phase 1} x:int;

+

+procedure {:yields} {:phase 1} p() 

+requires {:phase 1} x >= 5; 

+ensures {:phase 1} x >= 8; 

+{ 

+    call yield_x(5);

+    call Incr(1); 

+    call yield_x(6);

+    call Incr(1); 

+    call yield_x(7);

+    call Incr(1); 

+}

+

+procedure {:yields} {:phase 1} q() 

+{ 

+    call Incr(3); 

+}

+

+procedure {:yields} {:phase 0,1} Incr(val: int);

+ensures {:atomic}

+|{A:

+  x := x + val; return true;

+}|;

+

+procedure {:yields} {:phase 1} yield_x(n: int)

+requires {:phase 1} x >= n; 

+ensures {:phase 1} x >= n; 

+{

+    yield;

+    assert {:phase 1} x >= n;

+}
\ No newline at end of file
diff --git a/Test/og/Program2.bpl.expect b/Test/og/Program2.bpl.expect
new file mode 100644
index 00000000..5b2909f1
--- /dev/null
+++ b/Test/og/Program2.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 3 verified, 0 errors

diff --git a/Test/og/Program3.bpl b/Test/og/Program3.bpl
new file mode 100644
index 00000000..e1b014b7
--- /dev/null
+++ b/Test/og/Program3.bpl
@@ -0,0 +1,33 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+var {:phase 1} x:int;

+

+procedure {:yields} {:phase 1} p() 

+requires {:phase 1} x >= 5; 

+ensures {:phase 1} x >= 8; 

+{ 

+    call yield_x();

+    call Incr(1); 

+    call yield_x();

+    call Incr(1); 

+    call yield_x();

+    call Incr(1); 

+}

+

+procedure {:yields} {:phase 1} q() 

+{ 

+    call Incr(3); 

+}

+

+procedure {:yields} {:phase 0,1} Incr(val: int);

+ensures {:atomic}

+|{A:

+  x := x + val; return true;

+}|;

+

+procedure {:yields} {:phase 1} yield_x()

+ensures {:phase 1} x >= old(x); 

+{

+    yield;

+    assert {:phase 1} x >= old(x);

+}
\ No newline at end of file
diff --git a/Test/og/Program3.bpl.expect b/Test/og/Program3.bpl.expect
new file mode 100644
index 00000000..5b2909f1
--- /dev/null
+++ b/Test/og/Program3.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 3 verified, 0 errors

diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
new file mode 100644
index 00000000..6130b69b
--- /dev/null
+++ b/Test/og/Program4.bpl
@@ -0,0 +1,55 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+type Tid; 

+function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;

+function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;

+

+function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool

+{

+  MapConstBool(false)[x := true]

+}

+function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool

+{

+  x

+}

+

+var {:linear "tid"} {:phase 1} alloc:[Tid]bool; 

+var {:phase 1} a:[Tid]int;

+

+procedure Allocate() returns ({:linear "tid"} tid:Tid); 

+modifies alloc; 

+

+procedure {:yields} {:phase 1} main() { 

+    var {:linear "tid"} tid:Tid;

+

+    yield;

+    while (true) { 

+        call tid := Allocate(); 

+	async call P(tid); 

+	yield;

+    }

+    yield;

+}

+

+procedure {:yields} {:phase 1} P({:cnst "tid"} tid: Tid) 

+ensures {:phase 1} a[tid] == old(a)[tid] + 1; 

+{ 

+    var t:int;

+

+    call t := Read(tid); 

+    yield;

+    assert {:phase 1} t == a[tid]; 

+    call Write(tid, t + 1); 

+}

+

+procedure {:yields} {:phase 0,1} Read({:cnst "tid"} tid: Tid) returns (val: int);

+ensures {:atomic}

+|{A:

+  val := a[tid]; return true;

+}|;

+

+procedure {:yields} {:phase 0,1} Write({:cnst "tid"} tid: Tid, val: int);

+ensures {:atomic}

+|{A:

+  a[tid] := val; return true;

+}|;

diff --git a/Test/og/Program4.bpl.expect b/Test/og/Program4.bpl.expect
new file mode 100644
index 00000000..3de74d3e
--- /dev/null
+++ b/Test/og/Program4.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 2 verified, 0 errors

diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl
new file mode 100644
index 00000000..845bf1a4
--- /dev/null
+++ b/Test/og/Program5.bpl
@@ -0,0 +1,97 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+type Tid;

+const unique nil: Tid;

+function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;

+function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;

+

+var {:phase 0,3} Color:int;

+var {:phase 0,3} lock:Tid;

+

+function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool

+{

+  MapConstBool(false)[x := true]

+}

+function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool

+{

+  x

+}

+

+function {:inline} UNALLOC():int { 0 }

+function {:inline} WHITE():int { 1 }

+function {:inline} GRAY():int { 2 }

+function {:inline} BLACK():int { 3 }

+function {:inline} Unalloc(i:int) returns(bool) { i <= 0 }

+function {:inline} White(i:int) returns(bool) { i == 1 }

+function {:inline} Gray(i:int) returns(bool) { i == 2 }

+function {:inline} Black(i:int) returns(bool) { i >= 3 }

+

+procedure {:yields} {:phase 0,1} AcquireLock({:cnst "tid"} tid: Tid);

+  ensures {:right} |{ A: assert tid != nil; 

+                         assume lock == nil; 

+                         lock := tid; 

+                         return true; }|;

+

+procedure {:yields} {:phase 0,1} ReleaseLock({:cnst "tid"} tid: Tid);

+  ensures {:left} |{ A: assert tid != nil;

+                         assert lock == tid; 

+                         lock := nil; 

+                         return true; }|;

+

+procedure {:yields} {:phase 0,1} SetColorLocked({:cnst "tid"} tid:Tid, newCol:int); 

+  ensures {:atomic} |{A: assert tid != nil; assert lock == tid; Color := newCol; return true;}|;

+

+procedure {:yields} {:phase 0,1} GetColorLocked({:cnst "tid"} tid:Tid) returns (col:int);

+  ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|;

+

+procedure {:yields} {:phase 1,2} GetColorNoLock() returns (col:int);

+  ensures {:atomic} |{A: col := Color; return true;}|;

+

+procedure {:yields} {:phase 2} YieldColorOnlyGetsDarker()

+ensures {:phase 2} Color >= old(Color);

+{

+  yield;

+  assert {:phase 2} Color >= old(Color);

+}

+

+

+procedure {:yields} {:phase 2,3} TopWriteBarrier({:cnst "tid"} tid:Tid)

+ensures {:atomic} |{ A: assert tid != nil;

+                        goto B, C; 

+                     B: assume White(Color);

+                        Color := GRAY();

+                        return true; 

+                     C: return true;}|;

+{

+  var colorLocal:int;

+

+  yield;

+

+  call colorLocal := GetColorNoLock();

+  call YieldColorOnlyGetsDarker();

+  if (White(colorLocal)) {

+       call MidWriteBarrier(tid);

+  }

+

+  yield;

+}

+

+procedure {:yields} {:phase 1,2} MidWriteBarrier({:cnst "tid"} tid:Tid)

+ensures {:atomic} |{ A: assert tid != nil;

+                        goto B, C; 

+                     B: assume White(Color);

+                        Color := GRAY();

+                        return true; 

+                     C: return true;}|;

+{

+       var colorLocal:int;

+

+       yield;

+       call AcquireLock(tid);

+       call colorLocal := GetColorLocked(tid);

+       if (White(colorLocal)) {

+           call SetColorLocked(tid, GRAY());

+       } 

+       call ReleaseLock(tid);

+       yield;

+}
\ No newline at end of file
diff --git a/Test/og/Program5.bpl.expect b/Test/og/Program5.bpl.expect
new file mode 100644
index 00000000..d7c0ff95
--- /dev/null
+++ b/Test/og/Program5.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 18 verified, 0 errors