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/bitvectors/arrays.bpl | 4 ++-- Test/bitvectors/bv0.bpl | 4 ++-- Test/bitvectors/bv1.bpl | 4 ++-- Test/bitvectors/bv10.bpl | 4 ++-- Test/bitvectors/bv2.bpl | 4 ++-- Test/bitvectors/bv3.bpl | 4 ++-- Test/bitvectors/bv4.bpl | 4 ++-- Test/bitvectors/bv5.bpl | 4 ++-- Test/bitvectors/bv6.bpl | 4 ++-- Test/bitvectors/bv7.bpl | 4 ++-- Test/bitvectors/bv8.bpl | 4 ++-- Test/bitvectors/bv9.bpl | 4 ++-- 12 files changed, 24 insertions(+), 24 deletions(-) (limited to 'Test/bitvectors') diff --git a/Test/bitvectors/arrays.bpl b/Test/bitvectors/arrays.bpl index 17fc64a1..dae54e63 100644 --- a/Test/bitvectors/arrays.bpl +++ b/Test/bitvectors/arrays.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -proverWarnings:1 %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" const unique f1 : Field int; const unique f2 : Field bv32; const unique f3 : Field bool; diff --git a/Test/bitvectors/bv0.bpl b/Test/bitvectors/bv0.bpl index 18c6f5b8..8c330eda 100644 --- a/Test/bitvectors/bv0.bpl +++ b/Test/bitvectors/bv0.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -proverWarnings:1 %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" procedure foo2(x : bv32) returns(r : bv32) { block1: diff --git a/Test/bitvectors/bv1.bpl b/Test/bitvectors/bv1.bpl index 50c33cc3..2edc5037 100644 --- a/Test/bitvectors/bv1.bpl +++ b/Test/bitvectors/bv1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -proverWarnings:1 %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" procedure foo(x : bv32) returns(r : bv32) { var q : bv64; diff --git a/Test/bitvectors/bv10.bpl b/Test/bitvectors/bv10.bpl index 99ee6f86..cacf9f7a 100644 --- a/Test/bitvectors/bv10.bpl +++ b/Test/bitvectors/bv10.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" var x: bv32; procedure main() diff --git a/Test/bitvectors/bv2.bpl b/Test/bitvectors/bv2.bpl index 633c24e8..45fdf7e4 100644 --- a/Test/bitvectors/bv2.bpl +++ b/Test/bitvectors/bv2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -proverWarnings:1 %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" procedure foo2(x : bv32) returns(r : bv32) { block1: diff --git a/Test/bitvectors/bv3.bpl b/Test/bitvectors/bv3.bpl index 3c2d1034..5a2ce47f 100644 --- a/Test/bitvectors/bv3.bpl +++ b/Test/bitvectors/bv3.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -proverWarnings:1 %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" type bv; type bv16; diff --git a/Test/bitvectors/bv4.bpl b/Test/bitvectors/bv4.bpl index 71bc9fd1..29c8130a 100644 --- a/Test/bitvectors/bv4.bpl +++ b/Test/bitvectors/bv4.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -proverWarnings:1 %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" function a() returns(bv32); axiom a() == a(); diff --git a/Test/bitvectors/bv5.bpl b/Test/bitvectors/bv5.bpl index 48683f32..73dff1ad 100644 --- a/Test/bitvectors/bv5.bpl +++ b/Test/bitvectors/bv5.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" procedure P() returns () { var m : [a]int; diff --git a/Test/bitvectors/bv6.bpl b/Test/bitvectors/bv6.bpl index 7e943888..d0654b6f 100644 --- a/Test/bitvectors/bv6.bpl +++ b/Test/bitvectors/bv6.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" procedure Q() returns () { var x : bv32, y : bv16; diff --git a/Test/bitvectors/bv7.bpl b/Test/bitvectors/bv7.bpl index 77069bd8..a60f9547 100644 --- a/Test/bitvectors/bv7.bpl +++ b/Test/bitvectors/bv7.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -proverWarnings:1 %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" procedure foo2(x : bv32) returns(r : bv32) { block1: diff --git a/Test/bitvectors/bv8.bpl b/Test/bitvectors/bv8.bpl index bd50bc89..ee572998 100644 --- a/Test/bitvectors/bv8.bpl +++ b/Test/bitvectors/bv8.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" // This file includes some tests for which Boogie once generated bad Z3 input procedure foo() diff --git a/Test/bitvectors/bv9.bpl b/Test/bitvectors/bv9.bpl index 96275528..19a147ad 100644 --- a/Test/bitvectors/bv9.bpl +++ b/Test/bitvectors/bv9.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -proverOpt:OPTIMIZE_FOR_BV=true %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie -proverOpt:OPTIMIZE_FOR_BV=true "%s" > "%t" +// RUN: %diff "%s.expect" "%t" procedure foo(); implementation foo() -- cgit v1.2.3