diff options
| -rw-r--r-- | Test/og/DeviceCacheSimplified.bpl | 1 | ||||
| -rw-r--r-- | Test/og/DeviceCacheWithBuffer.bpl | 1 | ||||
| -rw-r--r-- | Test/og/async.bpl | 3 | ||||
| -rw-r--r-- | Test/og/houd1.bpl | 1 | ||||
| -rw-r--r-- | Test/og/lock-introduced.bpl | 1 | ||||
| -rw-r--r-- | Test/og/termination.bpl | 3 | ||||
| -rw-r--r-- | Test/og/treiber-stack.bpl | 3 | ||||
| -rw-r--r-- | Test/test21/Maps2.bpl | 1 | ||||
| -rw-r--r-- | Test/test21/test3_AddMethod_conv.bpl | 1 |
9 files changed, 12 insertions, 3 deletions
diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl index 3365e565..9e987b09 100644 --- a/Test/og/DeviceCacheSimplified.bpl +++ b/Test/og/DeviceCacheSimplified.bpl @@ -1,5 +1,6 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
// RUN: %diff %s.expect %t
+// XFAIL: *
type X;
function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
diff --git a/Test/og/DeviceCacheWithBuffer.bpl b/Test/og/DeviceCacheWithBuffer.bpl index a5252b87..be21ac7a 100644 --- a/Test/og/DeviceCacheWithBuffer.bpl +++ b/Test/og/DeviceCacheWithBuffer.bpl @@ -1,5 +1,6 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
// RUN: %diff %s.expect %t
+// XFAIL: *
type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
diff --git a/Test/og/async.bpl b/Test/og/async.bpl index 88307ba1..aef12331 100644 --- a/Test/og/async.bpl +++ b/Test/og/async.bpl @@ -1,5 +1,6 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
// RUN: %diff %s.expect %t
+// XFAIL: *
var {:phase 1} x: int;
var {:phase 1} y: int;
@@ -15,4 +16,4 @@ procedure {:yields} {:phase 1} P() requires x != y;
{
assert {:phase 1} x != y;
-}
\ No newline at end of file +}
diff --git a/Test/og/houd1.bpl b/Test/og/houd1.bpl index 03d52e54..421db3ff 100644 --- a/Test/og/houd1.bpl +++ b/Test/og/houd1.bpl @@ -1,5 +1,6 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
// RUN: %diff %s.expect %t
+// XFAIL: *
const {:existential true} b0: bool;
const {:existential true} b1: bool;
const {:existential true} b2: bool;
diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl index f0825c14..dd59ca7e 100644 --- a/Test/og/lock-introduced.bpl +++ b/Test/og/lock-introduced.bpl @@ -1,5 +1,6 @@ // 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/termination.bpl b/Test/og/termination.bpl index a7969e7c..fac2ecc7 100644 --- a/Test/og/termination.bpl +++ b/Test/og/termination.bpl @@ -1,5 +1,6 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
// RUN: %diff %s.expect %t
+// XFAIL: *
procedure {:yields} X();
ensures {:atomic 0} |{ A: return true; }|;
@@ -16,4 +17,4 @@ procedure {:yields} main() { }
yield;
assert {:phase 1} true;
-}
\ No newline at end of file +}
diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl index e082c4ca..7f962010 100644 --- a/Test/og/treiber-stack.bpl +++ b/Test/og/treiber-stack.bpl @@ -1,5 +1,6 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
// RUN: %diff %s.expect %t
+// XFAIL: *
type Node;
type lmap;
function {:linear "Node"} dom(lmap): [Node]bool;
@@ -76,4 +77,4 @@ procedure {:yields} pop() break;
}
}
-}
\ No newline at end of file +}
diff --git a/Test/test21/Maps2.bpl b/Test/test21/Maps2.bpl index 1a38ae48..ea020afd 100644 --- a/Test/test21/Maps2.bpl +++ b/Test/test21/Maps2.bpl @@ -4,6 +4,7 @@ // RUN: %diff %s.p.expect %t
// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
// RUN: %diff %s.a.expect %t
+// XFAIL: *
type T;
diff --git a/Test/test21/test3_AddMethod_conv.bpl b/Test/test21/test3_AddMethod_conv.bpl index ad4baba8..d0abb5c3 100644 --- a/Test/test21/test3_AddMethod_conv.bpl +++ b/Test/test21/test3_AddMethod_conv.bpl @@ -4,6 +4,7 @@ // RUN: %diff %s.p.expect %t
// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
// RUN: %diff %s.a.expect %t
+// XFAIL: *
// Spec# program verifier version 0.90, Copyright (c) 2003-2008, Microsoft.
// Command Line Options: /print:debug.txt AddMethod.dll
|