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

spaces.

29 files changed, 61 insertions, 61 deletions

diff --git a/Test/test0/Arrays0.bpl b/Test/test0/Arrays0.bpl
index 59ff8d14..6c208b1e 100644
--- a/Test/test0/Arrays0.bpl
+++ b/Test/test0/Arrays0.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 var one: [int]int;

 var two: [int,int]int;

 var three: [int,int,int]int;  // three's a crowd

diff --git a/Test/test0/Arrays1.bpl b/Test/test0/Arrays1.bpl
index bc7c89bb..4e031cb8 100644
--- a/Test/test0/Arrays1.bpl
+++ b/Test/test0/Arrays1.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noVerify %s | %OutputCheck %s

+// RUN: %boogie -noVerify "%s" | %OutputCheck "%s"

 var Q: [int,int][int]int;

 

 procedure P()

diff --git a/Test/test0/AttributeParsing.bpl b/Test/test0/AttributeParsing.bpl
index 0b99dc5f..afc0a88d 100644
--- a/Test/test0/AttributeParsing.bpl
+++ b/Test/test0/AttributeParsing.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify -print:- -env:0 %s > %t

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

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

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

 type {:sourcefile "test.ssc"} T; 

 

 function {:source "test.scc"} f(int) returns (int);

diff --git a/Test/test0/AttributeParsingErr.bpl b/Test/test0/AttributeParsingErr.bpl
index 7329289f..438f674d 100644
--- a/Test/test0/AttributeParsingErr.bpl
+++ b/Test/test0/AttributeParsingErr.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 type {:sourcefile "test.ssc"} {1} T; 

 

 function {:source "test.scc"} {1} f(int) returns (int);

diff --git a/Test/test0/AttributeResolution.bpl b/Test/test0/AttributeResolution.bpl
index eae2878e..e5094932 100644
--- a/Test/test0/AttributeResolution.bpl
+++ b/Test/test0/AttributeResolution.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 type {:sourcefile foo} T; 

 

 function {:source bar} f(int) returns (int);

diff --git a/Test/test0/BadLabels0.bpl b/Test/test0/BadLabels0.bpl
index ec6ff744..b3f6f896 100644
--- a/Test/test0/BadLabels0.bpl
+++ b/Test/test0/BadLabels0.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 procedure Dup(y: int)

 {

   X:

diff --git a/Test/test0/BadLabels1.bpl b/Test/test0/BadLabels1.bpl
index cbbe0f5e..d0b4e396 100644
--- a/Test/test0/BadLabels1.bpl
+++ b/Test/test0/BadLabels1.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 procedure P0()

 {

   // these labels don't exist at all

diff --git a/Test/test0/BadQuantifier.bpl b/Test/test0/BadQuantifier.bpl
index d202312e..db704a6e 100644
--- a/Test/test0/BadQuantifier.bpl
+++ b/Test/test0/BadQuantifier.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 

 function f(int) returns (bool);

 axiom (forall int x :: f(x) <== x >= 0);

diff --git a/Test/test0/EmptyCallArgs.bpl b/Test/test0/EmptyCallArgs.bpl
index aba48668..54b374d7 100644
--- a/Test/test0/EmptyCallArgs.bpl
+++ b/Test/test0/EmptyCallArgs.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 type C;

 

 procedure P(x:int, y:bool) returns (z:C);

diff --git a/Test/test0/LargeLiterals0.bpl b/Test/test0/LargeLiterals0.bpl
index b061688f..af9c02b4 100644
--- a/Test/test0/LargeLiterals0.bpl
+++ b/Test/test0/LargeLiterals0.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 // Test to parse large integer literals

 

 axiom 1234567890987654321 == 1234567890987654321;

diff --git a/Test/test0/LineParse.bpl b/Test/test0/LineParse.bpl
index ae11b419..76149ff6 100644
--- a/Test/test0/LineParse.bpl
+++ b/Test/test0/LineParse.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 #line

 #line 

 #line 0

diff --git a/Test/test0/LineResolve.bpl b/Test/test0/LineResolve.bpl
index 097943f5..da1a5bfa 100644
--- a/Test/test0/LineResolve.bpl
+++ b/Test/test0/LineResolve.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 procedure P() {

 var x: int;

 x :=

diff --git a/Test/test0/MapsResolutionErrors.bpl b/Test/test0/MapsResolutionErrors.bpl
index 8e5d5149..4cd5ff19 100644
--- a/Test/test0/MapsResolutionErrors.bpl
+++ b/Test/test0/MapsResolutionErrors.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 

 var m: []int;

 var p: <a>[]a;

diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl
index 05ab3c05..b3677621 100644
--- a/Test/test0/ModifiedBag.bpl
+++ b/Test/test0/ModifiedBag.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 // ----------- BEGIN PRELUDE

 

 

diff --git a/Test/test0/Orderings.bpl b/Test/test0/Orderings.bpl
index b14dbd4b..0d55ed27 100644
--- a/Test/test0/Orderings.bpl
+++ b/Test/test0/Orderings.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 

 type C;

 

diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl
index bc22e46d..8aa25d33 100644
--- a/Test/test0/PrettyPrint.bpl
+++ b/Test/test0/PrettyPrint.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify -printInstrumented %s > %t

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

+// RUN: %boogie -noVerify -printInstrumented "%s" > "%t"

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

 const x: int;

 const y: int;

 const z: int;

diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl
index 974bd9eb..d9e467ec 100644
--- a/Test/test0/Prog0.bpl
+++ b/Test/test0/Prog0.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 // BoogiePL Examples

 

 type elements;

diff --git a/Test/test0/Quoting.bpl b/Test/test0/Quoting.bpl
index 64564ad9..bf1f268e 100644
--- a/Test/test0/Quoting.bpl
+++ b/Test/test0/Quoting.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify -print:- -env:0 %s > %t

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

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

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

 function \true() returns(bool);

 

 type \procedure;

diff --git a/Test/test0/SeparateVerification0.bpl b/Test/test0/SeparateVerification0.bpl
index f598fe6f..a5c3962a 100644
--- a/Test/test0/SeparateVerification0.bpl
+++ b/Test/test0/SeparateVerification0.bpl
@@ -1,9 +1,9 @@
-// RUN: %boogie -noVerify %s > %t

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

-// RUN: %boogie -noVerify %s %s > %t

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

-// RUN: %boogie -noVerify %s %s SeparateVerification1.bpl > %t

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

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

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

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

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

+// RUN: %boogie -noVerify "%s" "%s" SeparateVerification1.bpl > "%t"

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

 // need to include this file twice for it to include all necessary declarations

 

 #if FILE_0

diff --git a/Test/test0/SeparateVerification1.bpl b/Test/test0/SeparateVerification1.bpl
index 683b24e1..5956828f 100644
--- a/Test/test0/SeparateVerification1.bpl
+++ b/Test/test0/SeparateVerification1.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s SeparateVerification0.bpl > %t

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

+// RUN: %boogie -noVerify "%s" SeparateVerification0.bpl > "%t"

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

 // to be used with SeparateVerification0.bpl

 

 // x and y are declared in SeparateVerification0.bpl

diff --git a/Test/test0/Triggers0.bpl b/Test/test0/Triggers0.bpl
index bbf37517..0113b992 100644
--- a/Test/test0/Triggers0.bpl
+++ b/Test/test0/Triggers0.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 // Trigger errors

 

 function f(int, int) returns (int);

diff --git a/Test/test0/Triggers1.bpl b/Test/test0/Triggers1.bpl
index bda65ea2..12d734be 100644
--- a/Test/test0/Triggers1.bpl
+++ b/Test/test0/Triggers1.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 // Trigger errors

 

 function f(int, int) returns (int);

diff --git a/Test/test0/Types0.bpl b/Test/test0/Types0.bpl
index 4e6e607b..62385acf 100644
--- a/Test/test0/Types0.bpl
+++ b/Test/test0/Types0.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 type T, U;

 type V;

 

diff --git a/Test/test0/Types1.bpl b/Test/test0/Types1.bpl
index 1e4d7033..75bb6178 100644
--- a/Test/test0/Types1.bpl
+++ b/Test/test0/Types1.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 type T, U;

 type V;

 

diff --git a/Test/test0/WhereParsing.bpl b/Test/test0/WhereParsing.bpl
index 6c203258..e75a1c81 100644
--- a/Test/test0/WhereParsing.bpl
+++ b/Test/test0/WhereParsing.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 const x: int;

 

 function R(int) returns (bool);

diff --git a/Test/test0/WhereParsing0.bpl b/Test/test0/WhereParsing0.bpl
index 7b3d21b2..da26bc5e 100644
--- a/Test/test0/WhereParsing0.bpl
+++ b/Test/test0/WhereParsing0.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 const x: int;

 

 function R(int) returns (bool);

diff --git a/Test/test0/WhereParsing1.bpl b/Test/test0/WhereParsing1.bpl
index 7be165d2..b65f7ce9 100644
--- a/Test/test0/WhereParsing1.bpl
+++ b/Test/test0/WhereParsing1.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 const x: int;

 

 function R(int) returns (bool);

diff --git a/Test/test0/WhereParsing2.bpl b/Test/test0/WhereParsing2.bpl
index e098036f..e7a0bd62 100644
--- a/Test/test0/WhereParsing2.bpl
+++ b/Test/test0/WhereParsing2.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 const x: int where x < 0;  // error: where clauses not allowed on constants

 

diff --git a/Test/test0/WhereResolution.bpl b/Test/test0/WhereResolution.bpl
index 0c2cf539..fac91dc8 100644
--- a/Test/test0/WhereResolution.bpl
+++ b/Test/test0/WhereResolution.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -noVerify %s > %t

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

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

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

 type double;

 

 function R(int) returns (bool);