From 02aca9ffab2d5a63e89f83d5eadb7133132c3b0a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 27 May 2014 20:53:49 +0100 Subject: Fix lit test suite when running Boogie under a path that contains spaces. --- Test/inline/Elevator.bpl | 6 +++--- Test/inline/InliningAndLoops.bpl | 4 ++-- Test/inline/codeexpr.bpl | 4 ++-- Test/inline/expansion2.bpl | 6 +++--- Test/inline/expansion3.bpl | 4 ++-- Test/inline/expansion4.bpl | 4 ++-- Test/inline/fundef.bpl | 4 ++-- Test/inline/fundef2.bpl | 4 ++-- Test/inline/polyInline.bpl | 6 +++--- Test/inline/test0.bpl | 4 ++-- Test/inline/test1.bpl | 4 ++-- Test/inline/test2.bpl | 4 ++-- Test/inline/test3.bpl | 4 ++-- Test/inline/test4.bpl | 4 ++-- Test/inline/test5.bpl | 4 ++-- Test/inline/test6.bpl | 4 ++-- 16 files changed, 35 insertions(+), 35 deletions(-) (limited to 'Test/inline') 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; { -- cgit v1.2.3