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

spaces.

16 files changed, 35 insertions, 35 deletions

diff --git a/Test/inline/Elevator.bpl b/Test/inline/Elevator.bpl
index 7a6b8128..2e146643 100644
--- a/Test/inline/Elevator.bpl
+++ b/Test/inline/Elevator.bpl
@@ -1,6 +1,6 @@
-// RUN: %boogie %s > %t

-// RUN: %boogie -removeEmptyBlocks:0 %s >> %t

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

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

+// RUN: %boogie -removeEmptyBlocks:0 "%s" >> "%t"

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

 // A Boogie version of Elevator.asml (see Boogie/Test/inline/Elevator.asml)

 

 var floors: [int]bool;  // set of integer

diff --git a/Test/inline/InliningAndLoops.bpl b/Test/inline/InliningAndLoops.bpl
index a22fd18c..74b20913 100644
--- a/Test/inline/InliningAndLoops.bpl
+++ b/Test/inline/InliningAndLoops.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -loopUnroll:3 -soundLoopUnrolling %s > %t

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

+// RUN: %boogie -loopUnroll:3 -soundLoopUnrolling "%s" > "%t"

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

 procedure foo(N: int)

   requires N == 2;

 {

diff --git a/Test/inline/codeexpr.bpl b/Test/inline/codeexpr.bpl
index f9cef515..0b4ebeb6 100644
--- a/Test/inline/codeexpr.bpl
+++ b/Test/inline/codeexpr.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie %s > %t

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

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

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

 var g: bool;

 

 procedure {:inline 1} bar() returns (l: bool) 

diff --git a/Test/inline/expansion2.bpl b/Test/inline/expansion2.bpl
index da13d50f..9883ce83 100644
--- a/Test/inline/expansion2.bpl
+++ b/Test/inline/expansion2.bpl
@@ -1,6 +1,6 @@
-// RUN: %boogie -proverLog:%T/expand2.sx %s > %t

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

-// RUN: %OutputCheck --file-to-check=%T/expand2.sx %s

+// RUN: %boogie "-proverLog:%T/expand2.sx" "%s" > "%t"

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

+// RUN: %OutputCheck "--file-to-check=%T/expand2.sx" "%s"

 function {:inline true} xxgz(x:int) returns(bool)

  { x > 0 }

 function {:inline true} xxf1(x:int,y:bool) returns(int)

diff --git a/Test/inline/expansion3.bpl b/Test/inline/expansion3.bpl
index 8d95166c..bfb8b0fa 100644
--- a/Test/inline/expansion3.bpl
+++ b/Test/inline/expansion3.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie %s > %t

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

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

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

 function {:inline true} foo3(x:int, y:bool) returns(bool)

  { foo3(x,y) }

 

diff --git a/Test/inline/expansion4.bpl b/Test/inline/expansion4.bpl
index c8bbe923..1c1ff51c 100644
--- a/Test/inline/expansion4.bpl
+++ b/Test/inline/expansion4.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie %s > %t

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

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

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

 function foo(x:int) : int

   { if x <= 0 then 1 else foo(x - 1) + 2 }

 

diff --git a/Test/inline/fundef.bpl b/Test/inline/fundef.bpl
index a7298c9c..9c5b2cfd 100644
--- a/Test/inline/fundef.bpl
+++ b/Test/inline/fundef.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -print:- -env:0 %s > %t

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

+// RUN: %boogie -print:- -env:0 "%s" > "%t"

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

 function {:inline true} foo(x:int) returns(bool)

   { x > 0 }

 function {:inline false} foo2(x:int) returns(bool)

diff --git a/Test/inline/fundef2.bpl b/Test/inline/fundef2.bpl
index 527d235d..39453453 100644
--- a/Test/inline/fundef2.bpl
+++ b/Test/inline/fundef2.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie %s > %t

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

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

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

 function {:inline true} foo(x:int) returns(bool)

   { x > 0 }

 

diff --git a/Test/inline/polyInline.bpl b/Test/inline/polyInline.bpl
index 1f6ea200..ed404867 100644
--- a/Test/inline/polyInline.bpl
+++ b/Test/inline/polyInline.bpl
@@ -1,6 +1,6 @@
-// RUN: %boogie /typeEncoding:predicates /logPrefix:p %s > %t

-// RUN: %boogie /typeEncoding:arguments /logPrefix:a %s >> %t

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

+// RUN: %boogie /typeEncoding:predicates /logPrefix:p "%s" > "%t"

+// RUN: %boogie /typeEncoding:arguments /logPrefix:a "%s" >> "%t"

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

 

 const C:int;

 const D:bool;

diff --git a/Test/inline/test0.bpl b/Test/inline/test0.bpl
index 9a547d77..6a2d9640 100644
--- a/Test/inline/test0.bpl
+++ b/Test/inline/test0.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie %s > %t

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

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

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

 // inlined functions

 

 function Twice(x: int) returns (int)

diff --git a/Test/inline/test1.bpl b/Test/inline/test1.bpl
index 1414978b..11ce6b4f 100644
--- a/Test/inline/test1.bpl
+++ b/Test/inline/test1.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t

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

+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"

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

 

 procedure Main()

 {

diff --git a/Test/inline/test2.bpl b/Test/inline/test2.bpl
index 7cafdf62..981d7604 100644
--- a/Test/inline/test2.bpl
+++ b/Test/inline/test2.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t

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

+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"

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

 

 var glb:int;

 

diff --git a/Test/inline/test3.bpl b/Test/inline/test3.bpl
index 3db73413..2f8b1749 100644
--- a/Test/inline/test3.bpl
+++ b/Test/inline/test3.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t

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

+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"

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

 

 var glb:int;

 

diff --git a/Test/inline/test4.bpl b/Test/inline/test4.bpl
index 248dfc6e..7743c498 100644
--- a/Test/inline/test4.bpl
+++ b/Test/inline/test4.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t

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

+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"

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

 

 procedure main(x:int)

 {

diff --git a/Test/inline/test5.bpl b/Test/inline/test5.bpl
index 8e092261..d7a80737 100644
--- a/Test/inline/test5.bpl
+++ b/Test/inline/test5.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie %s > %t

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

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

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

 // test a case, where the inlined proc comes before the caller

 

 procedure {:inline 2} foo()

diff --git a/Test/inline/test6.bpl b/Test/inline/test6.bpl
index febf1aae..d2e034fc 100644
--- a/Test/inline/test6.bpl
+++ b/Test/inline/test6.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer %s > %t

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

+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"

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

 procedure {:inline 2} foo()

   modifies x;

 {