Fix lit test suite when running Boogie under a path that contains

spaces.

27 files changed, 54 insertions, 54 deletions

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 59723dc8..62101cba 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 type X;

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

 const nil: X;

diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
index 9e987b09..afc3e91b 100644
--- a/Test/og/DeviceCacheSimplified.bpl
+++ b/Test/og/DeviceCacheSimplified.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 // XFAIL: *

 type X;

 

diff --git a/Test/og/DeviceCacheWithBuffer.bpl b/Test/og/DeviceCacheWithBuffer.bpl
index be21ac7a..a66dbaca 100644
--- a/Test/og/DeviceCacheWithBuffer.bpl
+++ b/Test/og/DeviceCacheWithBuffer.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// 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/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 4c664ec4..bbae8b04 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 type X;

 const nil: X;

 var {:phase 1} l: X;

diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index 37bba956..ce435c51 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

 

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

diff --git a/Test/og/async.bpl b/Test/og/async.bpl
index aef12331..2219fe8c 100644
--- a/Test/og/async.bpl
+++ b/Test/og/async.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 // XFAIL: *

 var {:phase 1} x: int;

 var {:phase 1} y: int;

diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index 26a4eb46..b348075e 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer %s > %t

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

+// RUN: %boogie -noinfer "%s" > "%t"

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

 var {:phase 1} g:int;

 

 procedure {:yields} {:phase 1} PB()

diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index 9d82e229..48394f92 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 type X;

 const nil: X;

 

diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index ba05d666..5ddc75c0 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer %s > %t

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

+// RUN: %boogie -noinfer "%s" > "%t"

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

 var {:phase 1} g:int;

 

 procedure {:yields} {:phase 1} PB()

diff --git a/Test/og/houd1.bpl b/Test/og/houd1.bpl
index 421db3ff..8c86f22b 100644
--- a/Test/og/houd1.bpl
+++ b/Test/og/houd1.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 // XFAIL: *

 const {:existential true} b0: bool;

 const {:existential true} b1: bool;

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index f6a4de75..de7c53e6 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 type X;

 function {:builtin "MapConst"} MapConstInt(int) : [X]int;

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

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index dff4936c..73ffb9ad 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 type X;

 function {:builtin "MapConst"} MapConstInt(int) : [X]int;

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

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

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

+// 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.bpl b/Test/og/lock.bpl
index 044cde1e..90357d4c 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 var {:phase 2} b: bool;

 

 procedure {:yields} {:phase 2} main()

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 2d1c53df..87538a20 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 var {:phase 2} b: int;

 

 procedure {:yields} {:phase 2} main()

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index f0a2fd5b..c54782e5 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 type X;

 

 const unique null : int;

diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index a691c087..ccddb25e 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;

 

 var {:phase 1} g:int;

diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index 190a024a..0fc6d32f 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer %s > %t

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

+// RUN: %boogie -noinfer "%s" > "%t"

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

 var {:phase 1} x:int;

 

 procedure {:yields} {:phase 0,1} Set(v: int);

diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index 90846b6c..1cd0a5c8 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer %s > %t

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

+// RUN: %boogie -noinfer "%s" > "%t"

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

 var {:phase 1} g:int;

 

 procedure {:yields} {:phase 1} PB()

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 52c2e913..8cc1c578 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

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

 

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

diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index 4bffcf94..60466d67 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 var {:phase 1} a:int;

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index 5f0b30bf..cfb593a6 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

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

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index 3f5adedd..b3c3e86d 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 var {:phase 1} x: int;

 function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;

 

diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index c4964c0e..02db387c 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

 

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

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

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 // XFAIL: *

 procedure {:yields} X();

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

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 3ee7485b..d532c5a2 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 function RightOpen(n: int) : [int]bool;

 function RightClosed(n: int) : [int]bool;

 axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);

diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl
index 7f962010..942bae67 100644
--- a/Test/og/treiber-stack.bpl
+++ b/Test/og/treiber-stack.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t

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

+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

 // XFAIL: *

 type Node;

 type lmap;