diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-27 20:53:49 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-27 20:53:49 +0100 |
| commit | 02aca9ffab2d5a63e89f83d5eadb7133132c3b0a (patch) | |
| tree | 673526b54101f72b42813d6f05edaba15f82b727 /Test/bitvectors | |
| parent | 75416c24e78d9992c10fbb86ba458e813acf943d (diff) | |
Fix lit test suite when running Boogie under a path that contains
spaces.
Diffstat (limited to 'Test/bitvectors')
| -rw-r--r-- | Test/bitvectors/arrays.bpl | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv0.bpl | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv1.bpl | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv10.bpl | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv2.bpl | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv3.bpl | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv4.bpl | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv5.bpl | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv6.bpl | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv7.bpl | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv8.bpl | 4 | ||||
| -rw-r--r-- | Test/bitvectors/bv9.bpl | 4 |
12 files changed, 24 insertions, 24 deletions
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>[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()
|