summaryrefslogtreecommitdiff
path: root/Test/test7
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test7')
-rw-r--r--Test/test7/MultipleErrors.bpl20
-rw-r--r--Test/test7/NestedVC.bpl4
-rw-r--r--Test/test7/UnreachableBlocks.bpl4
3 files changed, 14 insertions, 14 deletions
diff --git a/Test/test7/MultipleErrors.bpl b/Test/test7/MultipleErrors.bpl
index ac1f7e54..6f5944fc 100644
--- a/Test/test7/MultipleErrors.bpl
+++ b/Test/test7/MultipleErrors.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -vc:block -errorLimit:1 -errorTrace:1 -logPrefix:-1block %s > %t1
-// RUN: %diff %s.e1.block.expect %t1
-// RUN: %boogie -vc:local -errorLimit:1 -errorTrace:1 -logPrefix:-1local %s > %t2
-// RUN: %diff %s.e1.local.expect %t2
-// RUN: %boogie -vc:dag -errorLimit:1 -errorTrace:1 -logPrefix:-1dag %s > %t3
-// RUN: %diff %s.e1.dag.expect %t3
-// RUN: %boogie -vc:local -errorLimit:10 -errorTrace:1 -logPrefix:-10local %s > %t4
-// RUN: %diff %s.e10.local.expect %t4
-// RUN: %boogie -vc:dag -errorLimit:10 -errorTrace:1 -logPrefix:-10dag %s > %t5
-// RUN: %diff %s.e10.dag.expect %t5
+// RUN: %boogie -vc:block -errorLimit:1 -errorTrace:1 -logPrefix:-1block "%s" > "%t1"
+// RUN: %diff "%s.e1.block.expect" "%t1"
+// RUN: %boogie -vc:local -errorLimit:1 -errorTrace:1 -logPrefix:-1local "%s" > "%t2"
+// RUN: %diff "%s.e1.local.expect" "%t2"
+// RUN: %boogie -vc:dag -errorLimit:1 -errorTrace:1 -logPrefix:-1dag "%s" > "%t3"
+// RUN: %diff "%s.e1.dag.expect" "%t3"
+// RUN: %boogie -vc:local -errorLimit:10 -errorTrace:1 -logPrefix:-10local "%s" > "%t4"
+// RUN: %diff "%s.e10.local.expect" "%t4"
+// RUN: %boogie -vc:dag -errorLimit:10 -errorTrace:1 -logPrefix:-10dag "%s" > "%t5"
+// RUN: %diff "%s.e10.dag.expect" "%t5"
// Author of this comment: mikebarnett ec02177eefb5
// The following tests are rather fickle at the moment--different errors
diff --git a/Test/test7/NestedVC.bpl b/Test/test7/NestedVC.bpl
index be4e0483..6865be93 100644
--- a/Test/test7/NestedVC.bpl
+++ b/Test/test7/NestedVC.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -vc:nested %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -vc:nested "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure P()
{
A: goto B, C;
diff --git a/Test/test7/UnreachableBlocks.bpl b/Test/test7/UnreachableBlocks.bpl
index fd31ebe9..95c35029 100644
--- a/Test/test7/UnreachableBlocks.bpl
+++ b/Test/test7/UnreachableBlocks.bpl
@@ -1,5 +1,5 @@
-// RUN: %boogie -vc:nested %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -vc:nested "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// In the following program, block "A" has no dominator, which would cause Boogie
// to crash if Boogie didn't first remove unreachable blocks. That is essentially
// what this test tests