fixed some tests in og

added another test in linear (based on bug reported by Chris)
removed the QED build configuration

8 files changed, 65 insertions, 8 deletions

diff --git a/Test/linear/async-bug.bpl b/Test/linear/async-bug.bpl
new file mode 100644
index 00000000..faa1a65d
--- /dev/null
+++ b/Test/linear/async-bug.bpl
@@ -0,0 +1,31 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"

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

+const GcTid:int;

+

+procedure {:yields} {:phase 100} Initialize({:cnst "tid"} tid:int)

+requires{:phase 100} tid == GcTid;

+{

+    yield;

+    assert{:phase 100} tid == GcTid;

+

+    async call GarbageCollect(tid);

+

+    yield;

+    assert{:phase 100} tid == GcTid;

+

+    async call GarbageCollect(tid);

+

+    yield;

+    assert{:phase 100} tid == GcTid;

+

+    yield;

+    assert{:phase 100} tid == GcTid;

+}

+

+procedure {:yields} {:phase 100} GarbageCollect({:cnst "tid"} tid:int)

+requires{:phase 100} tid == GcTid;

+{

+    yield;

+    assert{:phase 100} tid == GcTid;

+}

+

diff --git a/Test/linear/async-bug.bpl.expect b/Test/linear/async-bug.bpl.expect
new file mode 100644
index 00000000..8bfe61d1
--- /dev/null
+++ b/Test/linear/async-bug.bpl.expect
@@ -0,0 +1,3 @@
+async-bug.bpl(11,10): Error: Const linear variable cannot be an argument for a const parameter of an async procedure call

+async-bug.bpl(16,10): Error: Const linear variable cannot be an argument for a const parameter of an async procedure call

+2 type checking errors detected in async-bug.bpl

diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl
index 33d84fa2..0b4e39f3 100644
--- a/Test/og/lock-introduced.bpl
+++ b/Test/og/lock-introduced.bpl
@@ -1,6 +1,5 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-// XFAIL: *

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

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

 {

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

+Boogie program verifier finished with 12 verified, 0 errors

diff --git a/Test/og/termination.bpl b/Test/og/termination.bpl
index 26ff030d..35064f77 100644
--- a/Test/og/termination.bpl
+++ b/Test/og/termination.bpl
@@ -1,17 +1,15 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-// XFAIL: *

-procedure {:yields} X();

-ensures {:atomic 0} |{ A: return true; }|;

+procedure {:yields} {:phase 0} X();

+ensures {:atomic} |{ A: return true; }|;

 

-procedure {:yields} Y();

-ensures {:left 0} |{ A: return true; }|;

+procedure {:yields} {:phase 0} Y();

+ensures {:left} |{ A: return true; }|;

 

-procedure {:yields} main() {

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

   yield;

   call X();

   while (*)

-//  invariant {:terminates} true;

   {

     call Y();

   }

diff --git a/Test/og/termination.bpl.expect b/Test/og/termination.bpl.expect
new file mode 100644
index 00000000..a924f8cf
--- /dev/null
+++ b/Test/og/termination.bpl.expect
@@ -0,0 +1,3 @@
+termination.bpl(9,31): Error: Loop at termination.bpl(12, 3) not simulated appropriately at phase 1
+

+1 type checking errors detected in termination.bpl

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

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

+procedure {:yields} {:phase 0} X();

+ensures {:atomic} |{ A: return true; }|;

+

+procedure {:yields} {:phase 0} Y();

+ensures {:left} |{ A: return true; }|;

+

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

+  yield;

+  call X();

+  while (*)

+  invariant {:terminates} {:phase 1} true;

+  {

+    call Y();

+  }

+  yield;

+  assert {:phase 1} true;

+}

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

+Boogie program verifier finished with 1 verified, 0 errors