fixed some tests in og

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

6 files changed, 31 insertions, 8 deletions

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