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 | |
| parent | 75416c24e78d9992c10fbb86ba458e813acf943d (diff) | |
Fix lit test suite when running Boogie under a path that contains
spaces.
325 files changed, 860 insertions, 840 deletions
diff --git a/Test/AbsHoudini/fail1.bpl b/Test/AbsHoudini/fail1.bpl index 5e15340c..02bcb8d3 100644 --- a/Test/AbsHoudini/fail1.bpl +++ b/Test/AbsHoudini/fail1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b1(x: bool) : bool;
var myVar: int;
diff --git a/Test/AbsHoudini/houd1.bpl b/Test/AbsHoudini/houd1.bpl index 0a8ebeb3..0bd4831a 100644 --- a/Test/AbsHoudini/houd1.bpl +++ b/Test/AbsHoudini/houd1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b1(x: bool) : bool;
var myVar: int;
diff --git a/Test/AbsHoudini/houd10.bpl b/Test/AbsHoudini/houd10.bpl index 6ee73b9a..5a0942cc 100644 --- a/Test/AbsHoudini/houd10.bpl +++ b/Test/AbsHoudini/houd10.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b1():bool;
function {:existential true} b2():bool;
function {:existential true} b3():bool;
diff --git a/Test/AbsHoudini/houd11.bpl b/Test/AbsHoudini/houd11.bpl index dbde4f37..638d8ec2 100644 --- a/Test/AbsHoudini/houd11.bpl +++ b/Test/AbsHoudini/houd11.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} Assert() : bool;
var fooVar: int;
diff --git a/Test/AbsHoudini/houd12.bpl b/Test/AbsHoudini/houd12.bpl index ac46ef62..12727d65 100644 --- a/Test/AbsHoudini/houd12.bpl +++ b/Test/AbsHoudini/houd12.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Example to test candidate annotations on loops
function {:existential true} Assert(): bool;
diff --git a/Test/AbsHoudini/houd2.bpl b/Test/AbsHoudini/houd2.bpl index c4d8e4e0..97a73464 100644 --- a/Test/AbsHoudini/houd2.bpl +++ b/Test/AbsHoudini/houd2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} Assert(x:bool) : bool;
function {:existential true} b1 (x:bool):bool;
function {:existential true} b2 (x:bool):bool;
diff --git a/Test/AbsHoudini/houd3.bpl b/Test/AbsHoudini/houd3.bpl index a37b5874..178c0e36 100644 --- a/Test/AbsHoudini/houd3.bpl +++ b/Test/AbsHoudini/houd3.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} Assert(x: bool) : bool;
function {:existential true} b1(x: bool) : bool;
function {:existential true} b2(x: bool) : bool;
diff --git a/Test/AbsHoudini/houd4.bpl b/Test/AbsHoudini/houd4.bpl index 2fc339d9..3268ce12 100644 --- a/Test/AbsHoudini/houd4.bpl +++ b/Test/AbsHoudini/houd4.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} Assert() : bool;
function {:existential true} b1():bool;
function {:existential true} b2(x:bool):bool;
diff --git a/Test/AbsHoudini/houd5.bpl b/Test/AbsHoudini/houd5.bpl index 8a08b5cf..9a4c274b 100644 --- a/Test/AbsHoudini/houd5.bpl +++ b/Test/AbsHoudini/houd5.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b1(x:bool):bool;
function {:existential true} b2(x:bool):bool;
function {:existential true} b3(x:bool):bool;
diff --git a/Test/AbsHoudini/houd6.bpl b/Test/AbsHoudini/houd6.bpl index 209e2f01..4d9cc9e8 100644 --- a/Test/AbsHoudini/houd6.bpl +++ b/Test/AbsHoudini/houd6.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b1():bool;
function {:existential true} b2():bool;
function {:existential true} b3():bool;
diff --git a/Test/AbsHoudini/houd7.bpl b/Test/AbsHoudini/houd7.bpl index 6df7b428..4035755c 100644 --- a/Test/AbsHoudini/houd7.bpl +++ b/Test/AbsHoudini/houd7.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b1():bool;
function {:existential true} b2():bool;
function {:existential true} b3():bool;
diff --git a/Test/AbsHoudini/houd8.bpl b/Test/AbsHoudini/houd8.bpl index e5b88466..dff155aa 100644 --- a/Test/AbsHoudini/houd8.bpl +++ b/Test/AbsHoudini/houd8.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b1():bool;
function {:existential true} b2():bool;
function {:existential true} b3():bool;
diff --git a/Test/AbsHoudini/pred1.bpl b/Test/AbsHoudini/pred1.bpl index 0c2d7f10..4db4810e 100644 --- a/Test/AbsHoudini/pred1.bpl +++ b/Test/AbsHoudini/pred1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b0(x:bool, y:bool): bool;
function {:existential true} b1(x:bool, y:bool): bool;
function {:existential true} b2(x:bool, y:bool): bool;
diff --git a/Test/AbsHoudini/pred2.bpl b/Test/AbsHoudini/pred2.bpl index 9e93495f..c9ac3f74 100644 --- a/Test/AbsHoudini/pred2.bpl +++ b/Test/AbsHoudini/pred2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b0(x:bool): bool;
var g: int;
diff --git a/Test/AbsHoudini/pred3.bpl b/Test/AbsHoudini/pred3.bpl index 1cb36798..38f42088 100644 --- a/Test/AbsHoudini/pred3.bpl +++ b/Test/AbsHoudini/pred3.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b0(x:bool, y:bool): bool;
function {:existential true} b1(x:bool, y:bool): bool;
function {:existential true} b2(x:bool, y:bool): bool;
diff --git a/Test/AbsHoudini/pred4.bpl b/Test/AbsHoudini/pred4.bpl index 9c814e3b..06e504e2 100644 --- a/Test/AbsHoudini/pred4.bpl +++ b/Test/AbsHoudini/pred4.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b1(x:bool, y:bool): bool;
function {:existential true} {:absdomain "Intervals"} b3(x:int): bool;
diff --git a/Test/AbsHoudini/pred5.bpl b/Test/AbsHoudini/pred5.bpl index 762a354f..1c96fe4d 100644 --- a/Test/AbsHoudini/pred5.bpl +++ b/Test/AbsHoudini/pred5.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} b1(x: bool) : bool;
procedure main()
diff --git a/Test/AbsHoudini/quant1.bpl b/Test/AbsHoudini/quant1.bpl index a5709736..c3a8814c 100644 --- a/Test/AbsHoudini/quant1.bpl +++ b/Test/AbsHoudini/quant1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} {:absdomain "IA[Intervals]"} b1(x: int) : bool;
procedure foo ()
diff --git a/Test/AbsHoudini/quant2.bpl b/Test/AbsHoudini/quant2.bpl index 2f291fca..1091155b 100644 --- a/Test/AbsHoudini/quant2.bpl +++ b/Test/AbsHoudini/quant2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
procedure main()
diff --git a/Test/AbsHoudini/quant3.bpl b/Test/AbsHoudini/quant3.bpl index 10fb72c7..951639ff 100644 --- a/Test/AbsHoudini/quant3.bpl +++ b/Test/AbsHoudini/quant3.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
procedure foo ()
diff --git a/Test/AbsHoudini/quant4.bpl b/Test/AbsHoudini/quant4.bpl index 99c37572..ac24d7ce 100644 --- a/Test/AbsHoudini/quant4.bpl +++ b/Test/AbsHoudini/quant4.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} {:absdomain "IA[HoudiniConst]"} b1() : bool;
procedure foo ()
diff --git a/Test/AbsHoudini/quant5.bpl b/Test/AbsHoudini/quant5.bpl index 83e6e68a..d511e9ac 100644 --- a/Test/AbsHoudini/quant5.bpl +++ b/Test/AbsHoudini/quant5.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
procedure foo ()
diff --git a/Test/AbsHoudini/test1.bpl b/Test/AbsHoudini/test1.bpl index ba18cf15..10015723 100644 --- a/Test/AbsHoudini/test1.bpl +++ b/Test/AbsHoudini/test1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var g: bool;
procedure foo()
diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl index 76a02e23..cb2fe89a 100644 --- a/Test/AbsHoudini/test10.bpl +++ b/Test/AbsHoudini/test10.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var sdv_7: int;
var sdv_21: int;
function {:existential true} b1(): bool;
diff --git a/Test/AbsHoudini/test2.bpl b/Test/AbsHoudini/test2.bpl index 8c1717bf..1272e7d9 100644 --- a/Test/AbsHoudini/test2.bpl +++ b/Test/AbsHoudini/test2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var g: int;
var h: int;
diff --git a/Test/AbsHoudini/test7.bpl b/Test/AbsHoudini/test7.bpl index d9500308..118a1c99 100644 --- a/Test/AbsHoudini/test7.bpl +++ b/Test/AbsHoudini/test7.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} Assert() : bool;
var g: int;
diff --git a/Test/AbsHoudini/test8.bpl b/Test/AbsHoudini/test8.bpl index 0b00bc19..f9a9afaa 100644 --- a/Test/AbsHoudini/test8.bpl +++ b/Test/AbsHoudini/test8.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:existential true} Assert(): bool;
var g: int;
diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl index 221234e5..7d624167 100644 --- a/Test/AbsHoudini/test9.bpl +++ b/Test/AbsHoudini/test9.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var v1: int;
var v2: int;
var v3: int;
diff --git a/Test/README.md b/Test/README.md index 4446aa4f..136881a5 100644 --- a/Test/README.md +++ b/Test/README.md @@ -108,22 +108,28 @@ considered to fail. The RUN lines may use several substitutions
- ``%boogie`` expands to the absolute path to the Boogie executable with any set
- options and prefixed by ``mono`` on non Windows platforms
+ options and prefixed by ``mono`` on non Windows platforms. This does not need
+ to be quoted.
- ``%diff`` expands to the diff tool being used. This is ``diff`` on non
Windows platforms and ``pydiff`` on Windows. Do not use the ``fc`` tool
- because it is buggy when tests are run concurrently.
+ because it is buggy when tests are run concurrently. This does not need to be
+ quoted.
-- ``%OutputCheck`` expands to the absolute path to the OutputCheck tool
+- ``%OutputCheck`` expands to the absolute path to the OutputCheck tool. This
+ does not need to be quoted.
-- ``%s`` the absolute path to the current test file
+- ``%s`` the absolute path to the current test file. You should make sure this
+ is quoted so that tests work correctly for users who use spaces in their file
+ paths.
-- ``%T`` the path to the temporary directory for this test
+- ``%T`` the path to the temporary directory for this test. You should make sure
+ this is quoted.
- ``%t`` expands to the absolute path of a filename that can be used as a
temporary file. This always expands to the same value in a single test so if
you need multiple different temporary files append a unique value (e.g.
- ``%t1``, ``%t2``... etc).
+ ``%t1``, ``%t2``... etc). You should make sure this is quoted.
Currently most tests simply execute boogie recording its output which then
compared to a file containing the expected output (``.expect`` files) using
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl index b9ff8269..565b6823 100644 --- a/Test/aitest0/Intervals.bpl +++ b/Test/aitest0/Intervals.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const N: int;
axiom 0 <= N;
diff --git a/Test/aitest0/constants.bpl b/Test/aitest0/constants.bpl index dbdc32d6..a3b82df7 100644 --- a/Test/aitest0/constants.bpl +++ b/Test/aitest0/constants.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Test the constant propagation AI
var GlobalFlag : bool;
diff --git a/Test/aitest1/Bound.bpl b/Test/aitest1/Bound.bpl index 7df27414..81b3635f 100644 --- a/Test/aitest1/Bound.bpl +++ b/Test/aitest1/Bound.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const TEST: name;
procedure P()
diff --git a/Test/aitest1/Linear0.bpl b/Test/aitest1/Linear0.bpl index 3a74b1e9..7e55fb12 100644 --- a/Test/aitest1/Linear0.bpl +++ b/Test/aitest1/Linear0.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Simple test file for checking the inference of linear constraints.
var x: int;
diff --git a/Test/aitest1/Linear1.bpl b/Test/aitest1/Linear1.bpl index 505d1a11..855dacae 100644 --- a/Test/aitest1/Linear1.bpl +++ b/Test/aitest1/Linear1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Simple test file for checking the inference of linear constraints.
var x: int;
diff --git a/Test/aitest1/Linear2.bpl b/Test/aitest1/Linear2.bpl index de1da8a1..fa743278 100644 --- a/Test/aitest1/Linear2.bpl +++ b/Test/aitest1/Linear2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Simple test file for checking the inference of linear constraints.
var x: int;
diff --git a/Test/aitest1/Linear3.bpl b/Test/aitest1/Linear3.bpl index 4b91bd0f..a71214fc 100644 --- a/Test/aitest1/Linear3.bpl +++ b/Test/aitest1/Linear3.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Simple test file for checking the inference of linear constraints.
var x: int;
diff --git a/Test/aitest1/Linear4.bpl b/Test/aitest1/Linear4.bpl index c3e908f2..6cd4a947 100644 --- a/Test/aitest1/Linear4.bpl +++ b/Test/aitest1/Linear4.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Simple test file for checking the inference of linear constraints.
var x: int;
diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl index 69cbb7a7..fdd961c3 100644 --- a/Test/aitest1/Linear5.bpl +++ b/Test/aitest1/Linear5.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Simple test file for checking the inference of linear constraints.
var x: int;
diff --git a/Test/aitest1/Linear6.bpl b/Test/aitest1/Linear6.bpl index 7d066435..a6747114 100644 --- a/Test/aitest1/Linear6.bpl +++ b/Test/aitest1/Linear6.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Simple test file for checking the inference of linear constraints.
var x: int;
diff --git a/Test/aitest1/Linear7.bpl b/Test/aitest1/Linear7.bpl index 45514a67..45ef3e79 100644 --- a/Test/aitest1/Linear7.bpl +++ b/Test/aitest1/Linear7.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Simple test file for checking the inference of linear constraints.
var x: int;
diff --git a/Test/aitest1/Linear8.bpl b/Test/aitest1/Linear8.bpl index 14f396ad..cb86b72f 100644 --- a/Test/aitest1/Linear8.bpl +++ b/Test/aitest1/Linear8.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure foo () returns ()
{
diff --git a/Test/aitest1/Linear9.bpl b/Test/aitest1/Linear9.bpl index 1352bfb0..86687f05 100644 --- a/Test/aitest1/Linear9.bpl +++ b/Test/aitest1/Linear9.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure foo () returns ()
{
var i: int;
diff --git a/Test/aitest1/ineq.bpl b/Test/aitest1/ineq.bpl index 030c435c..47f1e4f1 100644 --- a/Test/aitest1/ineq.bpl +++ b/Test/aitest1/ineq.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Test the polyhedra domain for linear inequalities
diff --git a/Test/aitest9/TestIntervals.bpl b/Test/aitest9/TestIntervals.bpl index 6d968bc9..307a1da4 100644 --- a/Test/aitest9/TestIntervals.bpl +++ b/Test/aitest9/TestIntervals.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s -infer:j > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" -infer:j > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure P()
{
var a: int, b: int, c: int;
diff --git a/Test/aitest9/VarMapFixpoint.bpl b/Test/aitest9/VarMapFixpoint.bpl index 1ee8d694..6a051ed9 100644 --- a/Test/aitest9/VarMapFixpoint.bpl +++ b/Test/aitest9/VarMapFixpoint.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s -infer:j > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" -infer:j > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure main()
{
var x: int, y: int, z: int;
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()
diff --git a/Test/codeexpr/CodeExpr0.bpl b/Test/codeexpr/CodeExpr0.bpl index 58568cea..97dd60e7 100644 --- a/Test/codeexpr/CodeExpr0.bpl +++ b/Test/codeexpr/CodeExpr0.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()
{
assert |{ A: return true; }|;
diff --git a/Test/codeexpr/CodeExpr1.bpl b/Test/codeexpr/CodeExpr1.bpl index 20617cc8..4e8faf3f 100644 --- a/Test/codeexpr/CodeExpr1.bpl +++ b/Test/codeexpr/CodeExpr1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// ------ the good ------
procedure F(x: int, y: int) returns (z: bool)
diff --git a/Test/codeexpr/CodeExpr2.bpl b/Test/codeexpr/CodeExpr2.bpl index f42ed4f2..9d8beed7 100644 --- a/Test/codeexpr/CodeExpr2.bpl +++ b/Test/codeexpr/CodeExpr2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type T;
const zero: T;
diff --git a/Test/datatypes/ex.bpl b/Test/datatypes/ex.bpl index 854119e0..e7a0e694 100644 --- a/Test/datatypes/ex.bpl +++ b/Test/datatypes/ex.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -typeEncoding:m %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type{:datatype} finite_map;
function{:constructor} finite_map(dom:[int]bool, map:[int]int):finite_map;
diff --git a/Test/datatypes/t1.bpl b/Test/datatypes/t1.bpl index 77276bb8..f0488639 100644 --- a/Test/datatypes/t1.bpl +++ b/Test/datatypes/t1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -typeEncoding:m %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type TT;
type {:datatype} Tree;
function {:constructor} leaf() : Tree;
diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl index 227ceb41..106b8d0c 100644 --- a/Test/datatypes/t2.bpl +++ b/Test/datatypes/t2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -typeEncoding:m %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type TT;
type {:datatype} Tree;
function {:constructor} leaf`0() : Tree;
diff --git a/Test/extractloops/detLoopExtract.bpl b/Test/extractloops/detLoopExtract.bpl index b224aece..7e9d0629 100644 --- a/Test/extractloops/detLoopExtract.bpl +++ b/Test/extractloops/detLoopExtract.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -deterministicExtractLoops -recursionBound:4 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -deterministicExtractLoops -recursionBound:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var g:int; var h:int; //not modified var k:int; //modified in a procedure call diff --git a/Test/extractloops/detLoopExtract1.bpl b/Test/extractloops/detLoopExtract1.bpl index 80646ef2..3791fab8 100644 --- a/Test/extractloops/detLoopExtract1.bpl +++ b/Test/extractloops/detLoopExtract1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -deterministicExtractLoops -recursionBound:4 %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -deterministicExtractLoops -recursionBound:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" var g:int; procedure {:entrypoint} Foo(a:int) diff --git a/Test/extractloops/t1.bpl b/Test/extractloops/t1.bpl index 2f566a4c..a0ebb0b8 100644 --- a/Test/extractloops/t1.bpl +++ b/Test/extractloops/t1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var g: int;
diff --git a/Test/extractloops/t2.bpl b/Test/extractloops/t2.bpl index 5546eb86..d62733f7 100644 --- a/Test/extractloops/t2.bpl +++ b/Test/extractloops/t2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var g: int;
diff --git a/Test/extractloops/t3.bpl b/Test/extractloops/t3.bpl index d3afa8d5..023a9adb 100644 --- a/Test/extractloops/t3.bpl +++ b/Test/extractloops/t3.bpl @@ -1,7 +1,7 @@ -// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:2 %s > %t
-// RUN: %diff %s.rb2.expect %t
-// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:4 %s > %t
-// RUN: %diff %s.rb4.expect %t
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:2 "%s" > "%t"
+// RUN: %diff "%s.rb2.expect" "%t"
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:4 "%s" > "%t"
+// RUN: %diff "%s.rb4.expect" "%t"
var g: int;
procedure foo()
diff --git a/Test/generalizedarray/Maps.bpl b/Test/generalizedarray/Maps.bpl index f240bbc7..24521194 100644 --- a/Test/generalizedarray/Maps.bpl +++ b/Test/generalizedarray/Maps.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type X;
function {:builtin "MapAdd"} mapadd([X]int, [X]int) : [X]int;
diff --git a/Test/havoc0/KbdCreateClassObject.bpl b/Test/havoc0/KbdCreateClassObject.bpl index 35892d41..df0f5039 100644 --- a/Test/havoc0/KbdCreateClassObject.bpl +++ b/Test/havoc0/KbdCreateClassObject.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -monomorphize %s > %t
-// RUN: %diff success.expect %t
+// RUN: %boogie -monomorphize "%s" > "%t"
+// RUN: %diff success.expect "%t"
type byte, name;
function OneByteToInt(byte) returns (int);
function TwoBytesToInt(byte, byte) returns (int);
diff --git a/Test/havoc0/KeyboardClassFindMorePorts.bpl b/Test/havoc0/KeyboardClassFindMorePorts.bpl index a2324310..a2b8994d 100644 --- a/Test/havoc0/KeyboardClassFindMorePorts.bpl +++ b/Test/havoc0/KeyboardClassFindMorePorts.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -monomorphize %s > %t
-// RUN: %diff success.expect %t
+// RUN: %boogie -monomorphize "%s" > "%t"
+// RUN: %diff success.expect "%t"
type byte, name;
function OneByteToInt(byte) returns (int);
function TwoBytesToInt(byte, byte) returns (int);
diff --git a/Test/havoc0/KeyboardClassUnload.bpl b/Test/havoc0/KeyboardClassUnload.bpl index 83aba916..3ca87200 100644 --- a/Test/havoc0/KeyboardClassUnload.bpl +++ b/Test/havoc0/KeyboardClassUnload.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -monomorphize %s > %t
-// RUN: %diff success.expect %t
+// RUN: %boogie -monomorphize "%s" > "%t"
+// RUN: %diff success.expect "%t"
type byte, name;
function OneByteToInt(byte) returns (int);
function TwoBytesToInt(byte, byte) returns (int);
diff --git a/Test/havoc0/MouCreateClassObject.bpl b/Test/havoc0/MouCreateClassObject.bpl index 62f1276b..98a0fda6 100644 --- a/Test/havoc0/MouCreateClassObject.bpl +++ b/Test/havoc0/MouCreateClassObject.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -monomorphize %s > %t
-// RUN: %diff success.expect %t
+// RUN: %boogie -monomorphize "%s" > "%t"
+// RUN: %diff success.expect "%t"
type byte, name;
function OneByteToInt(byte) returns (int);
function TwoBytesToInt(byte, byte) returns (int);
diff --git a/Test/havoc0/MouseClassFindMorePorts.bpl b/Test/havoc0/MouseClassFindMorePorts.bpl index 56b24b26..f9e4a18c 100644 --- a/Test/havoc0/MouseClassFindMorePorts.bpl +++ b/Test/havoc0/MouseClassFindMorePorts.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -monomorphize %s > %t
-// RUN: %diff success.expect %t
+// RUN: %boogie -monomorphize "%s" > "%t"
+// RUN: %diff success.expect "%t"
type byte, name;
function OneByteToInt(byte) returns (int);
function TwoBytesToInt(byte, byte) returns (int);
diff --git a/Test/havoc0/MouseClassUnload.bpl b/Test/havoc0/MouseClassUnload.bpl index 047a6c54..97f92fe5 100644 --- a/Test/havoc0/MouseClassUnload.bpl +++ b/Test/havoc0/MouseClassUnload.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -monomorphize %s > %t
-// RUN: %diff success.expect %t
+// RUN: %boogie -monomorphize "%s" > "%t"
+// RUN: %diff success.expect "%t"
type byte, name;
function OneByteToInt(byte) returns (int);
function TwoBytesToInt(byte, byte) returns (int);
diff --git a/Test/houdini/houd1.bpl b/Test/houdini/houd1.bpl index 91ff47d4..0ad0feee 100644 --- a/Test/houdini/houd1.bpl +++ b/Test/houdini/houd1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const {:existential true} b1:bool;
var myVar: int;
diff --git a/Test/houdini/houd10.bpl b/Test/houdini/houd10.bpl index c1e0c823..11757320 100644 --- a/Test/houdini/houd10.bpl +++ b/Test/houdini/houd10.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const {:existential true} b1:bool;
const {:existential true} b2:bool;
const {:existential true} b3:bool;
diff --git a/Test/houdini/houd11.bpl b/Test/houdini/houd11.bpl index 22f7bfd1..dc90f900 100644 --- a/Test/houdini/houd11.bpl +++ b/Test/houdini/houd11.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var fooVar: int;
diff --git a/Test/houdini/houd12.bpl b/Test/houdini/houd12.bpl index a3379a2e..7e39b8af 100644 --- a/Test/houdini/houd12.bpl +++ b/Test/houdini/houd12.bpl @@ -1,4 +1,4 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s | %OutputCheck -d %s
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" | %OutputCheck -d "%s"
// Example to test candidate annotations on loops
// CHECK-L: Assignment computed by Houdini:
diff --git a/Test/houdini/houd2.bpl b/Test/houdini/houd2.bpl index 1f89e762..e0bfe4ba 100644 --- a/Test/houdini/houd2.bpl +++ b/Test/houdini/houd2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const {:existential true} b1:bool;
const {:existential true} b2:bool;
diff --git a/Test/houdini/houd3.bpl b/Test/houdini/houd3.bpl index cc634450..2f6b1452 100644 --- a/Test/houdini/houd3.bpl +++ b/Test/houdini/houd3.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const {:existential true} b1:bool;
const {:existential true} b2:bool;
diff --git a/Test/houdini/houd4.bpl b/Test/houdini/houd4.bpl index e85d6047..0950e422 100644 --- a/Test/houdini/houd4.bpl +++ b/Test/houdini/houd4.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const {:existential true} b1:bool;
const {:existential true} b2:bool;
const {:existential true} b3:bool;
diff --git a/Test/houdini/houd5.bpl b/Test/houdini/houd5.bpl index 8a696a40..b6ee32dd 100644 --- a/Test/houdini/houd5.bpl +++ b/Test/houdini/houd5.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const {:existential true} b1:bool;
const {:existential true} b2:bool;
const {:existential true} b3:bool;
diff --git a/Test/houdini/houd6.bpl b/Test/houdini/houd6.bpl index cf67383f..a1dc7220 100644 --- a/Test/houdini/houd6.bpl +++ b/Test/houdini/houd6.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const {:existential true} b1:bool;
const {:existential true} b2:bool;
const {:existential true} b3:bool;
diff --git a/Test/houdini/houd7.bpl b/Test/houdini/houd7.bpl index ba3b5cda..6238ee5a 100644 --- a/Test/houdini/houd7.bpl +++ b/Test/houdini/houd7.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const {:existential true} b1:bool;
const {:existential true} b2:bool;
const {:existential true} b3:bool;
diff --git a/Test/houdini/houd8.bpl b/Test/houdini/houd8.bpl index 4b4c9afb..52d49111 100644 --- a/Test/houdini/houd8.bpl +++ b/Test/houdini/houd8.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const {:existential true} b1:bool;
const {:existential true} b2:bool;
const {:existential true} b3:bool;
diff --git a/Test/houdini/houd9.bpl b/Test/houdini/houd9.bpl index 4dbfb4aa..0a33896c 100644 --- a/Test/houdini/houd9.bpl +++ b/Test/houdini/houd9.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const {:existential true} b1:bool;
const {:existential true} b2:bool;
const {:existential true} b3:bool;
diff --git a/Test/houdini/test1.bpl b/Test/houdini/test1.bpl index 89d5d50d..7a8db5e8 100644 --- a/Test/houdini/test1.bpl +++ b/Test/houdini/test1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var g: bool;
procedure foo()
diff --git a/Test/houdini/test10.bpl b/Test/houdini/test10.bpl index 33cc54d9..f77d0c87 100644 --- a/Test/houdini/test10.bpl +++ b/Test/houdini/test10.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var sdv_7: int;
var sdv_21: int;
const {:existential true} b1: bool;
diff --git a/Test/houdini/test2.bpl b/Test/houdini/test2.bpl index 99897758..5639dc61 100644 --- a/Test/houdini/test2.bpl +++ b/Test/houdini/test2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var g: int;
var h: int;
diff --git a/Test/houdini/test7.bpl b/Test/houdini/test7.bpl index be369db9..4f0a832d 100644 --- a/Test/houdini/test7.bpl +++ b/Test/houdini/test7.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var g: int;
procedure main()
diff --git a/Test/houdini/test8.bpl b/Test/houdini/test8.bpl index c92d63fe..79738a9b 100644 --- a/Test/houdini/test8.bpl +++ b/Test/houdini/test8.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var g: int;
procedure main()
diff --git a/Test/houdini/test9.bpl b/Test/houdini/test9.bpl index f2eae609..68404a8f 100644 --- a/Test/houdini/test9.bpl +++ b/Test/houdini/test9.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var v1: int;
var v2: int;
var v3: int;
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;
{
diff --git a/Test/linear/allocator.bpl b/Test/linear/allocator.bpl index ae8f517d..31f54f7e 100644 --- a/Test/linear/allocator.bpl +++ b/Test/linear/allocator.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure A({:linear "tid"} i': int) returns ({:linear "tid"} i: int);
ensures i == i';
diff --git a/Test/linear/bug.bpl b/Test/linear/bug.bpl index a619968e..9177e2ca 100644 --- a/Test/linear/bug.bpl +++ b/Test/linear/bug.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
function {:inline} {:linear ""} LinearIntDistinctness(x:int) : [int]bool { MapConstBool(false)[x := true] }
diff --git a/Test/linear/f1.bpl b/Test/linear/f1.bpl index 513b67fa..e18fab9f 100644 --- a/Test/linear/f1.bpl +++ b/Test/linear/f1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
const {:existential true} b0: bool;
const {:existential true} b1: bool;
diff --git a/Test/linear/f2.bpl b/Test/linear/f2.bpl index 9517e349..16863154 100644 --- a/Test/linear/f2.bpl +++ b/Test/linear/f2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool;
diff --git a/Test/linear/f3.bpl b/Test/linear/f3.bpl index 1f29cc86..f5e08277 100644 --- a/Test/linear/f3.bpl +++ b/Test/linear/f3.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure A() {}
procedure B({:linear ""} tid:int) returns({:linear ""} tid':int)
diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl index d11f9d5c..72f165fb 100644 --- a/Test/linear/list.bpl +++ b/Test/linear/list.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type X;
function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl index 72067494..a3980a3e 100644 --- a/Test/linear/typecheck.bpl +++ b/Test/linear/typecheck.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type X;
procedure A()
diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg index e103edde..de51b761 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -56,6 +56,18 @@ config.environment['PYTHON_EXECUTABLE'] = getattr(config, 'python_executable', ' if config.test_exec_root is None: lit_config.fatal('Could not determine execution root for tests!') +""" + Function for quoting filepaths + so that if they contain spaces + lit's shell interpreter will + treat the path as a single argument +""" +def quotePath(path): + if ' ' in path: + return '"{path}"'.format(path=path) + else: + return path + ### Add Boogie specific substitutions # Find Boogie.exe @@ -71,6 +83,8 @@ boogieExecutable = os.path.join( binaryDir, 'Boogie.exe') if not os.path.exists(boogieExecutable): lit_config.fatal('Could not find Boogie.exe at {}'.format(boogieExecutable)) +boogieExecutable = quotePath(boogieExecutable) + if os.name == 'posix': boogieExecutable = 'mono ' + boogieExecutable if lit.util.which('mono') == None: @@ -116,7 +130,7 @@ diffExecutable = None if os.name == 'posix': diffExecutable = 'diff' + commonDiffFlags elif os.name == 'nt': - pydiff = os.path.join(config.test_source_root, 'pydiff.py') + pydiff = quotePath( os.path.join(config.test_source_root, 'pydiff.py') ) diffExecutable = sys.executable + ' ' + pydiff + commonDiffFlags else: lit_config.fatal('Unsupported platform') diff --git a/Test/livevars/NestedOneDimensionalMap.bpl b/Test/livevars/NestedOneDimensionalMap.bpl index 23667a6f..5f67f352 100644 --- a/Test/livevars/NestedOneDimensionalMap.bpl +++ b/Test/livevars/NestedOneDimensionalMap.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var k: int;
var AllMaps__1: [int][int]int;
diff --git a/Test/livevars/TwoDimensionalMap.bpl b/Test/livevars/TwoDimensionalMap.bpl index 9bf99e88..2a90ffe2 100644 --- a/Test/livevars/TwoDimensionalMap.bpl +++ b/Test/livevars/TwoDimensionalMap.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var k: int;
var AllMaps__1: [int,int]int;
diff --git a/Test/livevars/bla1.bpl b/Test/livevars/bla1.bpl index 97ae746a..669f8571 100644 --- a/Test/livevars/bla1.bpl +++ b/Test/livevars/bla1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var __storm_thread_done_0 : bool;
var __storm_thread_done_1 : bool;
var __storm_thread_done_2 : bool;
diff --git a/Test/livevars/daytona_bug2_ioctl_example_1.bpl b/Test/livevars/daytona_bug2_ioctl_example_1.bpl index ee71af7c..c752df09 100644 --- a/Test/livevars/daytona_bug2_ioctl_example_1.bpl +++ b/Test/livevars/daytona_bug2_ioctl_example_1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var __storm_thread_done_0 : bool;
var __storm_thread_done_1 : bool;
var __storm_thread_done_2 : bool;
diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl b/Test/livevars/daytona_bug2_ioctl_example_2.bpl index 3ef1e332..e170cda7 100644 --- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl +++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var __storm_thread_done_0 : bool;
var __storm_thread_done_1 : bool;
var __storm_thread_done_2 : bool;
diff --git a/Test/livevars/stack_overflow.bpl b/Test/livevars/stack_overflow.bpl index 22ccd875..aec86556 100644 --- a/Test/livevars/stack_overflow.bpl +++ b/Test/livevars/stack_overflow.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var raiseException : bool;
var errorReached : bool;
diff --git a/Test/lock/Lock.bpl b/Test/lock/Lock.bpl index ab7f20fe..54cd4853 100644 --- a/Test/lock/Lock.bpl +++ b/Test/lock/Lock.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure LockingExample();
implementation LockingExample()
diff --git a/Test/lock/LockIncorrect.bpl b/Test/lock/LockIncorrect.bpl index cffcc256..4bd86bbe 100644 --- a/Test/lock/LockIncorrect.bpl +++ b/Test/lock/LockIncorrect.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure LockingExample();
implementation LockingExample()
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index 59723dc8..62101cba 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl index 9e987b09..afc3e91b 100644 --- a/Test/og/DeviceCacheSimplified.bpl +++ b/Test/og/DeviceCacheSimplified.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// XFAIL: *
type X;
diff --git a/Test/og/DeviceCacheWithBuffer.bpl b/Test/og/DeviceCacheWithBuffer.bpl index be21ac7a..a66dbaca 100644 --- a/Test/og/DeviceCacheWithBuffer.bpl +++ b/Test/og/DeviceCacheWithBuffer.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// XFAIL: *
type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl index 4c664ec4..bbae8b04 100644 --- a/Test/og/FlanaganQadeer.bpl +++ b/Test/og/FlanaganQadeer.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type X;
const nil: X;
var {:phase 1} l: X;
diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl index 37bba956..ce435c51 100644 --- a/Test/og/akash.bpl +++ b/Test/og/akash.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
diff --git a/Test/og/async.bpl b/Test/og/async.bpl index aef12331..2219fe8c 100644 --- a/Test/og/async.bpl +++ b/Test/og/async.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// XFAIL: *
var {:phase 1} x: int;
var {:phase 1} y: int;
diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl index 26a4eb46..b348075e 100644 --- a/Test/og/bar.bpl +++ b/Test/og/bar.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var {:phase 1} g:int;
procedure {:yields} {:phase 1} PB()
diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl index 9d82e229..48394f92 100644 --- a/Test/og/civl-paper.bpl +++ b/Test/og/civl-paper.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type X;
const nil: X;
diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl index ba05d666..5ddc75c0 100644 --- a/Test/og/foo.bpl +++ b/Test/og/foo.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var {:phase 1} g:int;
procedure {:yields} {:phase 1} PB()
diff --git a/Test/og/houd1.bpl b/Test/og/houd1.bpl index 421db3ff..8c86f22b 100644 --- a/Test/og/houd1.bpl +++ b/Test/og/houd1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// XFAIL: *
const {:existential true} b0: bool;
const {:existential true} b1: bool;
diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl index f6a4de75..de7c53e6 100644 --- a/Test/og/linear-set.bpl +++ b/Test/og/linear-set.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type X;
function {:builtin "MapConst"} MapConstInt(int) : [X]int;
function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl index dff4936c..73ffb9ad 100644 --- a/Test/og/linear-set2.bpl +++ b/Test/og/linear-set2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type X;
function {:builtin "MapConst"} MapConstInt(int) : [X]int;
function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl index dd59ca7e..33d84fa2 100644 --- a/Test/og/lock-introduced.bpl +++ b/Test/og/lock-introduced.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// XFAIL: *
function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl index 044cde1e..90357d4c 100644 --- a/Test/og/lock.bpl +++ b/Test/og/lock.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var {:phase 2} b: bool;
procedure {:yields} {:phase 2} main()
diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl index 2d1c53df..87538a20 100644 --- a/Test/og/lock2.bpl +++ b/Test/og/lock2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var {:phase 2} b: int;
procedure {:yields} {:phase 2} main()
diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl index f0a2fd5b..c54782e5 100644 --- a/Test/og/multiset.bpl +++ b/Test/og/multiset.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type X;
const unique null : int;
diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl index a691c087..ccddb25e 100644 --- a/Test/og/new1.bpl +++ b/Test/og/new1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
var {:phase 1} g:int;
diff --git a/Test/og/one.bpl b/Test/og/one.bpl index 190a024a..0fc6d32f 100644 --- a/Test/og/one.bpl +++ b/Test/og/one.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var {:phase 1} x:int;
procedure {:yields} {:phase 0,1} Set(v: int);
diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl index 90846b6c..1cd0a5c8 100644 --- a/Test/og/parallel1.bpl +++ b/Test/og/parallel1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var {:phase 1} g:int;
procedure {:yields} {:phase 1} PB()
diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl index 52c2e913..8cc1c578 100644 --- a/Test/og/parallel2.bpl +++ b/Test/og/parallel2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var {:phase 1} a:[int]int;
function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl index 4bffcf94..60466d67 100644 --- a/Test/og/parallel4.bpl +++ b/Test/og/parallel4.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var {:phase 1} a:int;
procedure Allocate() returns ({:linear "tid"} xls: int);
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl index 5f0b30bf..cfb593a6 100644 --- a/Test/og/parallel5.bpl +++ b/Test/og/parallel5.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var {:phase 1} a:[int]int;
procedure Allocate() returns ({:linear "tid"} xls: int);
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl index 3f5adedd..b3c3e86d 100644 --- a/Test/og/perm.bpl +++ b/Test/og/perm.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var {:phase 1} x: int;
function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;
diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl index c4964c0e..02db387c 100644 --- a/Test/og/t1.bpl +++ b/Test/og/t1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
diff --git a/Test/og/termination.bpl b/Test/og/termination.bpl index fac2ecc7..26ff030d 100644 --- a/Test/og/termination.bpl +++ b/Test/og/termination.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// XFAIL: *
procedure {:yields} X();
ensures {:atomic 0} |{ A: return true; }|;
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index 3ee7485b..d532c5a2 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function RightOpen(n: int) : [int]bool;
function RightClosed(n: int) : [int]bool;
axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);
diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl index 7f962010..942bae67 100644 --- a/Test/og/treiber-stack.bpl +++ b/Test/og/treiber-stack.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// XFAIL: *
type Node;
type lmap;
diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl index 24c9d5ea..80b50686 100644 --- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl +++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -typeEncoding:m -z3multipleErrors %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var v4.Mem: [name][int]int;
var v4.alloc: int;
diff --git a/Test/prover/z3mutl.bpl b/Test/prover/z3mutl.bpl index b184a6a4..f42f7bb4 100644 --- a/Test/prover/z3mutl.bpl +++ b/Test/prover/z3mutl.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -typeEncoding:m -z3multipleErrors %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var x:int;
procedure Foo(){
diff --git a/Test/smoke/smoke0.bpl b/Test/smoke/smoke0.bpl index 7fb4f6fe..87531c8d 100644 --- a/Test/smoke/smoke0.bpl +++ b/Test/smoke/smoke0.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -smoke %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -smoke "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure a(x:int)
{
var y : int;
diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot index fe5c1b23..0a4ef6d9 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -verifySnapshots -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl > %t -// RUN: %diff %s.expect %t +// RUN: %boogie -verifySnapshots -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/stratifiedinline/bar1.bpl b/Test/stratifiedinline/bar1.bpl index 48cef01f..fdce8177 100644 --- a/Test/stratifiedinline/bar1.bpl +++ b/Test/stratifiedinline/bar1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var x: int;
var y: int;
diff --git a/Test/stratifiedinline/bar10.bpl b/Test/stratifiedinline/bar10.bpl index 3ec0f72f..477cfb04 100644 --- a/Test/stratifiedinline/bar10.bpl +++ b/Test/stratifiedinline/bar10.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var i: int;
var m: int;
diff --git a/Test/stratifiedinline/bar11.bpl b/Test/stratifiedinline/bar11.bpl index 4d1fffa0..b25d8451 100644 --- a/Test/stratifiedinline/bar11.bpl +++ b/Test/stratifiedinline/bar11.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var x: int;
var y: int;
procedure boogie_si_record_int(x:int);
diff --git a/Test/stratifiedinline/bar12.bpl b/Test/stratifiedinline/bar12.bpl index a129a02b..b11daa52 100644 --- a/Test/stratifiedinline/bar12.bpl +++ b/Test/stratifiedinline/bar12.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:inline} f(a:bool) : bool { true }
procedure {:entrypoint} main()
diff --git a/Test/stratifiedinline/bar13.bpl b/Test/stratifiedinline/bar13.bpl index fc4f35b0..7c8cc9bd 100644 --- a/Test/stratifiedinline/bar13.bpl +++ b/Test/stratifiedinline/bar13.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var alloc: int;
var assertsPassed: bool;
procedure boogie_si_record_li2bpl_int(x: int);
diff --git a/Test/stratifiedinline/bar2.bpl b/Test/stratifiedinline/bar2.bpl index 2f680760..a4f367de 100644 --- a/Test/stratifiedinline/bar2.bpl +++ b/Test/stratifiedinline/bar2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure foo() returns (x: bool)
{
var b: bool;
diff --git a/Test/stratifiedinline/bar3.bpl b/Test/stratifiedinline/bar3.bpl index 60fc8989..4625552b 100644 --- a/Test/stratifiedinline/bar3.bpl +++ b/Test/stratifiedinline/bar3.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var y: int;
var x: int;
diff --git a/Test/stratifiedinline/bar4.bpl b/Test/stratifiedinline/bar4.bpl index 8e439288..948683f8 100644 --- a/Test/stratifiedinline/bar4.bpl +++ b/Test/stratifiedinline/bar4.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var y: int;
var x: int;
diff --git a/Test/stratifiedinline/bar6.bpl b/Test/stratifiedinline/bar6.bpl index 33a06462..d763a82c 100644 --- a/Test/stratifiedinline/bar6.bpl +++ b/Test/stratifiedinline/bar6.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var M: [int]int;
procedure bar(y: int) returns (b: bool)
diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl index 531f9f43..1c83fb68 100644 --- a/Test/stratifiedinline/bar7.bpl +++ b/Test/stratifiedinline/bar7.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var i: int;
var m: int;
diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl index a1c63b72..e46b24e7 100644 --- a/Test/stratifiedinline/bar8.bpl +++ b/Test/stratifiedinline/bar8.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var i: int;
var m: int;
diff --git a/Test/stratifiedinline/bar9.bpl b/Test/stratifiedinline/bar9.bpl index da89dbf3..e5a84185 100644 --- a/Test/stratifiedinline/bar9.bpl +++ b/Test/stratifiedinline/bar9.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var i: int;
var m: int;
diff --git a/Test/stratifiedinline/large.bpl b/Test/stratifiedinline/large.bpl index 44e4e7fc..eae7c81a 100644 --- a/Test/stratifiedinline/large.bpl +++ b/Test/stratifiedinline/large.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure proc63() returns (nVar5796: int, nVar5797: bool);
modifies nVar2, nVar1, nVar3, nVar4, nVar5, nVar6, nVar7, nVar8, nVar9, nVar10, nVar11, nVar12, nVar13, nVar14, nVar15, nVar16, nVar17, nVar18, nVar19, nVar20, nVar21, nVar22, nVar23, nVar24, nVar25, nVar26, nVar27, nVar28, nVar29, nVar30, nVar31, nVar32, nVar33, nVar34, nVar35, nVar36, nVar37, nVar38, nVar39, nVar40, nVar41, nVar42, nVar43, nVar44, nVar45, nVar46, nVar47, nVar48, nVar49, nVar50, nVar51, nVar52, nVar53, nVar54, nVar55, nVar56, nVar57, nVar58, nVar59, nVar60, nVar61, nVar62, nVar63, nVar64, nVar65, nVar66, nVar67, nVar68, nVar69, nVar70, nVar71, nVar72, nVar73, nVar74, nVar75, nVar76, nVar77, nVar78, nVar79, nVar80, nVar81, nVar82, nVar83, nVar84, nVar85, nVar86, nVar87, nVar88, nVar89, nVar90, nVar91, nVar92, nVar93, nVar94, nVar95, nVar96, nVar97, nVar98, nVar99, nVar100, nVar101, nVar102, nVar103, nVar104, nVar105, nVar106, nVar107, nVar108, nVar109, nVar110, nVar111, nVar112, nVar113, nVar114, nVar115, nVar116, nVar117, nVar118, nVar119, nVar120, nVar121, nVar122, nVar123, nVar124, nVar125, nVar126, nVar127, nVar128, nVar129, nVar130, nVar131, nVar132, nVar133, nVar134, nVar135, nVar136, nVar137, nVar138, nVar139, nVar140, nVar141, nVar142, nVar143, nVar144, nVar145, nVar146, nVar147, nVar148, nVar149, nVar150, nVar151, nVar152, nVar153, nVar154, nVar155, nVar156, nVar157, nVar158, nVar159, nVar160, nVar161, nVar162, nVar163, nVar164, nVar165, nVar166, nVar167, nVar168, nVar169, nVar170, nVar171, nVar172, nVar173, nVar174, nVar175, nVar176, nVar177, nVar178, nVar179, nVar180, nVar181, nVar182, nVar183, nVar184, nVar185, nVar186, nVar187, nVar188, nVar189, nVar190, nVar191, nVar192, nVar193, nVar194, nVar195, nVar196, nVar197, nVar198, nVar199, nVar200, nVar201, nVar202, nVar203, nVar204, nVar205, nVar206, nVar207, nVar208, nVar209, nVar210, nVar211, nVar212, nVar213, nVar214, nVar215, nVar216, nVar217, nVar218, nVar219, nVar220, nVar221, nVar222, nVar223, nVar224, nVar225, nVar226, nVar227, nVar228, nVar229, nVar230, nVar231, nVar232, nVar233, nVar234, nVar235, nVar236, nVar237, nVar238, nVar239, nVar240, nVar241, nVar242, nVar243, nVar244, nVar245, nVar246, nVar247, nVar248, nVar249, nVar250, nVar251, nVar252, nVar253, nVar254, nVar255, nVar256, nVar257, nVar258, nVar259, nVar260, nVar261, nVar262, nVar263, nVar264, nVar265, nVar266, nVar267, nVar268, nVar269, nVar270, nVar271, nVar272, nVar273, nVar274, nVar275, nVar276, nVar277, nVar278, nVar279, nVar281, nVar282, nVar283, nVar284, nVar285, nVar286, nVar287, nVar288, nVar289, nVar290, nVar291, nVar292, nVar293, nVar294, nVar295, nVar296, nVar297, nVar298, nVar299, nVar300, nVar301, nVar302, nVar303, nVar304, nVar305, nVar306, nVar307, nVar308, nVar309, nVar310, nVar311, nVar312, nVar313, nVar314, nVar315, nVar316, nVar317, nVar318, nVar319, nVar320, nVar321, nVar322, nVar323, nVar324, nVar325, nVar326, nVar327, nVar328, nVar329, nVar330, nVar331, nVar332, nVar333, nVar334, nVar335, nVar336, nVar337, nVar338, nVar339, nVar340, nVar341, nVar342, nVar343, nVar344, nVar345, nVar346, nVar348, nVar349, nVar350, nVar351, nVar352, nVar353, nVar354, nVar355, nVar356, nVar357, nVar358, nVar359, nVar360, nVar361, nVar362, nVar363, nVar364, nVar365, nVar366, nVar367, nVar368, nVar369, nVar370, nVar371, nVar372, nVar373, nVar374, nVar375, nVar376, nVar377, nVar378, nVar379, nVar380, nVar381, nVar382, nVar383, nVar384, nVar385, nVar386, nVar387, nVar388, nVar389, nVar390, nVar391, nVar392, nVar393, nVar394, nVar395, nVar396, nVar397, nVar398, nVar400, nVar401, nVar402, nVar403, nVar404, nVar405, nVar406, nVar407, nVar408, nVar409, nVar410, nVar411, nVar412, nVar413, nVar414, nVar415, nVar416, nVar417, nVar418, nVar419, nVar420, nVar421, nVar422, nVar423, nVar424, nVar425, nVar426, nVar427, nVar428, nVar429, nVar430, nVar431, nVar432, nVar433, nVar434, nVar435, nVar436, nVar437, nVar438, nVar439, nVar440, nVar441, nVar442, nVar443, nVar444, nVar445, nVar446, nVar447, nVar448, nVar449, nVar450, nVar451, nVar452, nVar453, nVar454, nVar455, nVar456, nVar457, nVar458, nVar459, nVar460, nVar461, nVar462, nVar463, nVar464, nVar465, nVar466, nVar467, nVar468, nVar469, nVar470, nVar471, nVar472, nVar473, nVar474, nVar475, nVar476, nVar477, nVar478, nVar479, nVar480, nVar481, nVar482, nVar483, nVar484, nVar485, nVar486, nVar487, nVar488, nVar489, nVar490, nVar491, nVar492, nVar493, nVar494, nVar495, nVar496, nVar497, nVar498, nVar499, nVar500, nVar501, nVar502, nVar503, nVar504, nVar505, nVar506, nVar507, nVar508, nVar509, nVar510, nVar511, nVar512, nVar513, nVar514, nVar515, nVar516, nVar517, nVar518, nVar519, nVar520, nVar521, nVar522, nVar523, nVar524, nVar525, nVar526, nVar527, nVar528, nVar529, nVar530, nVar531, nVar532, nVar533, nVar534, nVar535, nVar536, nVar537, nVar538, nVar539, nVar540, nVar541, nVar542, nVar543, nVar544, nVar545, nVar546, nVar547, nVar548, nVar549, nVar550, nVar551, nVar552, nVar553, nVar554, nVar555, nVar556, nVar557, nVar558, nVar559, nVar560, nVar561, nVar562, nVar563, nVar564, nVar565, nVar566, nVar567, nVar568, nVar569, nVar570, nVar571, nVar572, nVar573, nVar574, nVar575, nVar576, nVar577, nVar578, nVar579, nVar580, nVar581, nVar582, nVar583, nVar584, nVar585, nVar586, nVar587, nVar588, nVar589, nVar590, nVar591, nVar592, nVar593, nVar594, nVar595, nVar596, nVar597, nVar598, nVar599, nVar600, nVar601, nVar602, nVar603, nVar604, nVar605, nVar606, nVar607, nVar608, nVar609, nVar610, nVar611, nVar612, nVar613, nVar614, nVar615, nVar616, nVar617, nVar618, nVar619, nVar620, nVar621, nVar622, nVar623, nVar624, nVar625, nVar626, nVar627, nVar628, nVar629, nVar630, nVar631, nVar632, nVar633, nVar634, nVar635, nVar636, nVar637, nVar638, nVar639, nVar640, nVar641, nVar642, nVar643, nVar644, nVar645, nVar646, nVar647, nVar648, nVar649, nVar650, nVar651, nVar652, nVar653, nVar654, nVar655, nVar656, nVar657, nVar658, nVar659, nVar660, nVar661, nVar662, nVar663, nVar664, nVar665, nVar666, nVar667, nVar668, nVar669, nVar670, nVar671, nVar672, nVar673, nVar674, nVar675, nVar676, nVar677, nVar678, nVar679, nVar680, nVar681, nVar682, nVar683, nVar684, nVar685, nVar686, nVar687, nVar688, nVar689, nVar690, nVar691, nVar692, nVar693, nVar694, nVar695, nVar696, nVar697, nVar698, nVar699, nVar700, nVar701, nVar702, nVar703, nVar704, nVar705, nVar706, nVar707, nVar708, nVar709, nVar710, nVar711, nVar712, nVar713, nVar714, nVar715, nVar716, nVar717, nVar718, nVar719, nVar720, nVar721, nVar722, nVar723, nVar724, nVar725, nVar726, nVar727, nVar728, nVar729, nVar730, nVar731, nVar732, nVar733, nVar734, nVar735, nVar736, nVar737, nVar738, nVar739, nVar740, nVar741, nVar742, nVar743, nVar744, nVar745, nVar746, nVar747, nVar748, nVar749, nVar750, nVar751, nVar752, nVar753, nVar754, nVar755, nVar756, nVar757, nVar758, nVar759, nVar760, nVar761, nVar762, nVar763, nVar764, nVar765, nVar766, nVar767, nVar768, nVar769, nVar770, nVar771, nVar772, nVar773, nVar774, nVar775, nVar776, nVar777, nVar778, nVar779, nVar780, nVar781, nVar782, nVar783, nVar784, nVar785, nVar786, nVar787, nVar788, nVar789, nVar790, nVar791, nVar792, nVar793, nVar794, nVar795, nVar796, nVar797, nVar798, nVar799, nVar800, nVar801, nVar802, nVar803, nVar804, nVar805, nVar806, nVar807, nVar808, nVar809, nVar810, nVar811, nVar812, nVar813, nVar814, nVar815, nVar816, nVar817, nVar818, nVar819, nVar820, nVar821, nVar822, nVar823, nVar824, nVar825, nVar826, nVar827, nVar828, nVar829, nVar830, nVar831, nVar832, nVar833, nVar834, nVar835, nVar836, nVar837, nVar838, nVar839, nVar840, nVar841, nVar842, nVar843, nVar844, nVar845, nVar846, nVar847, nVar848, nVar849, nVar850, nVar851, nVar852, nVar853, nVar854, nVar855, nVar856, nVar857, nVar858, nVar859, nVar860, nVar861, nVar862, nVar863, nVar864, nVar865, nVar866, nVar867, nVar868, nVar869, nVar870, nVar871, nVar872, nVar873, nVar874, nVar875, nVar876, nVar877, nVar878, nVar879, nVar880, nVar881, nVar882, nVar883, nVar884, nVar885, nVar886, nVar887, nVar888, nVar889, nVar890, nVar891, nVar892, nVar893, nVar894, nVar895, nVar896, nVar897, nVar898, nVar899, nVar900, nVar901, nVar902, nVar903, nVar904, nVar905, nVar906, nVar907, nVar908, nVar909, nVar910, nVar911, nVar912, nVar913, nVar914, nVar915, nVar916, nVar917, nVar918, nVar919, nVar920, nVar921, nVar922, nVar923, nVar924, nVar925, nVar926, nVar927, nVar928, nVar929, nVar930, nVar931, nVar932, nVar933, nVar934, nVar935, nVar936, nVar937, nVar938, nVar939, nVar940, nVar941, nVar942, nVar943, nVar944, nVar945, nVar946, nVar947, nVar948, nVar949, nVar950, nVar951, nVar952, nVar953, nVar954, nVar955, nVar956, nVar957, nVar958, nVar959, nVar960, nVar961, nVar962, nVar963, nVar964, nVar965, nVar966, nVar967, nVar968, nVar969, nVar970, nVar971, nVar972, nVar973, nVar974, nVar975, nVar976, nVar977, nVar978, nVar979, nVar980, nVar981, nVar982, nVar983, nVar984, nVar985, nVar986, nVar987, nVar988, nVar989, nVar990, nVar991, nVar992, nVar993, nVar994, nVar995, nVar996, nVar997, nVar998, nVar999, nVar1000, nVar1001, nVar1002, nVar1003, nVar1004, nVar1005, nVar1006, nVar1007, nVar1008, nVar1009, nVar1010, nVar1011, nVar1012, nVar1013, nVar1014, nVar1015, nVar1016, nVar1017, nVar1018, nVar1019, nVar1020, nVar1021, nVar1022, nVar1023, nVar1024, nVar1025, nVar1026, nVar1027, nVar1028, nVar1029, nVar1030, nVar1031, nVar1032, nVar1033, nVar1034, nVar1035, nVar1036, nVar1037, nVar1038, nVar1039, nVar1041, nVar1042, nVar1043, nVar1044, nVar1045, nVar1046, nVar1047, nVar1048, nVar1049, nVar1050, nVar1051, nVar1052, nVar1053, nVar1054, nVar1055, nVar1056, nVar1057, nVar1058, nVar1059, nVar1060, nVar1061, nVar1062, nVar1063, nVar1064, nVar1065, nVar1066, nVar1067, nVar1068, nVar1069, nVar1070, nVar1071, nVar1072, nVar1073, nVar1074, nVar1075, nVar1076, nVar1077, nVar1078, nVar1079, nVar1080, nVar1081, nVar1082, nVar1083, nVar1084, nVar1085, nVar1086, nVar1087, nVar1088, nVar1089, nVar1090, nVar1091, nVar1092, nVar1093, nVar1094, nVar1095, nVar1096, nVar1097, nVar1098, nVar1099, nVar1100, nVar1101, nVar1102, nVar1103, nVar1104, nVar1105, nVar1106, nVar1107, nVar1108, nVar1109, nVar1110, nVar1111, nVar1112, nVar1113, nVar1114, nVar1115, nVar1116, nVar1117, nVar1118, nVar1119, nVar1120, nVar1121, nVar1122, nVar1123, nVar1124, nVar1125, nVar1126, nVar1127, nVar1128, nVar1129, nVar1130, nVar1131, nVar1132, nVar1133, nVar1134, nVar1135, nVar1136, nVar1137, nVar1138, nVar1139, nVar1140, nVar1141, nVar1142, nVar1143, nVar1144, nVar1145, nVar1146, nVar1147, nVar1148, nVar1149, nVar1150, nVar1151, nVar1152, nVar1153, nVar1154, nVar1155, nVar1156, nVar1157, nVar1158, nVar1159, nVar1160, nVar1161, nVar1162, nVar1163, nVar1164, nVar1165, nVar1166, nVar1167, nVar1168, nVar1169, nVar1170, nVar1171, nVar1172, nVar1173, nVar1174, nVar1176, nVar1177, nVar1178, nVar1179, nVar1180, nVar1181, nVar1182, nVar1183, nVar1184, nVar1185, nVar1186, nVar1187, nVar1188, nVar1189, nVar1190, nVar1191, nVar1192, nVar1193, nVar1194, nVar1195, nVar1196, nVar1197, nVar1198, nVar1199, nVar1200, nVar1201, nVar1202, nVar1203, nVar1204, nVar1205, nVar1206, nVar1207, nVar1208, nVar1209, nVar1210, nVar1211, nVar1212, nVar1213, nVar1214, nVar1215, nVar1216, nVar1217, nVar1218, nVar1219, nVar1220, nVar1221, nVar1222, nVar1223, nVar1224, nVar1225, nVar1226, nVar1227, nVar1228, nVar1229, nVar1230, nVar1231, nVar1232, nVar1233, nVar1234, nVar1235, nVar1236, nVar1237, nVar1238, nVar1239, nVar1240, nVar1241, nVar1242, nVar1243, nVar1244, nVar1245, nVar1246, nVar1247, nVar1248, nVar1249, nVar1250, nVar1251, nVar1252, nVar1253, nVar1255, nVar1256, nVar1257, nVar1258, nVar1259, nVar1260, nVar1261, nVar1262, nVar1263, nVar1264, nVar1265, nVar1266, nVar1267, nVar1268, nVar1269, nVar1270, nVar1271, nVar1272, nVar1273, nVar1274, nVar1275, nVar1276, nVar1277, nVar1278, nVar1279, nVar1280, nVar1281, nVar1282, nVar1283, nVar1284, nVar1285, nVar1286, nVar1287, nVar1288, nVar1289, nVar1290, nVar1291, nVar1292, nVar1293, nVar1294, nVar1295, nVar1296, nVar1297, nVar1298, nVar1299, nVar1300, nVar1301, nVar1302, nVar1303, nVar1304, nVar1305, nVar1306, nVar1307, nVar1308, nVar1309, nVar1310, nVar1311, nVar1312, nVar1313, nVar1314, nVar1315, nVar1316, nVar1317, nVar1318, nVar1319, nVar1320, nVar1321, nVar1322, nVar1323, nVar1324, nVar1325, nVar1326, nVar1327, nVar1328, nVar1329, nVar1330, nVar1331, nVar1332, nVar1333, nVar1334, nVar1335, nVar1336, nVar1337, nVar1338, nVar1339, nVar1340, nVar1341, nVar1342, nVar1343, nVar1344, nVar1345, nVar1346, nVar1347, nVar1348, nVar1349, nVar1350, nVar1351, nVar1352, nVar1353, nVar1354, nVar1355, nVar1356, nVar1357, nVar1358, nVar1359, nVar1360, nVar1361, nVar1362, nVar1363, nVar1364, nVar1365, nVar1366, nVar1367, nVar1368, nVar1369, nVar1370, nVar1371, nVar1372, nVar1373, nVar1374, nVar1375, nVar1376, nVar1377, nVar1378, nVar1379, nVar1380, nVar1381, nVar1382, nVar1383, nVar1384, nVar1385, nVar1386, nVar1387, nVar1388, nVar1389, nVar1390, nVar1391, nVar1392, nVar1393, nVar1394, nVar1395, nVar1396, nVar1397, nVar1398, nVar1399, nVar1400, nVar1401, nVar1402, nVar1403, nVar1404, nVar1405, nVar1406, nVar1407, nVar1408, nVar1409, nVar1410, nVar1411, nVar1412, nVar1413, nVar1414, nVar1415, nVar1416, nVar1417, nVar1418, nVar1419, nVar1420, nVar1421, nVar1422, nVar1423, nVar1424, nVar1425, nVar1426, nVar1427, nVar1428, nVar1429, nVar1430, nVar1431, nVar1432, nVar1433, nVar1434, nVar1435, nVar1436, nVar1437, nVar1438, nVar1439, nVar1440, nVar1441, nVar1442, nVar1443, nVar1444, nVar1445, nVar1446, nVar1447, nVar1448, nVar1449, nVar1450, nVar1451, nVar1452, nVar1453, nVar1454, nVar1455, nVar1456, nVar1457, nVar1458, nVar1459, nVar1460, nVar1461, nVar1462, nVar1463, nVar1464, nVar1465, nVar1466, nVar1467, nVar1468, nVar1469, nVar1470, nVar1471, nVar1472, nVar1473, nVar1474, nVar1475, nVar1476, nVar1477, nVar1478, nVar1479, nVar1480, nVar1481, nVar1482, nVar1483, nVar1484, nVar1485, nVar1486, nVar1487, nVar1488, nVar1489, nVar1490, nVar1491, nVar1492, nVar1493, nVar1494, nVar1495, nVar1496, nVar1497, nVar1498, nVar1499, nVar1500, nVar1501, nVar1502, nVar1503, nVar1504, nVar1505, nVar1506, nVar1507, nVar1508, nVar1509, nVar1510, nVar1511, nVar1512, nVar1513, nVar1514, nVar1515, nVar1516, nVar1517, nVar1518, nVar1519, nVar1520, nVar1521, nVar1522, nVar1523, nVar1524, nVar1525, nVar1526, nVar1527, nVar1528, nVar1529, nVar1530, nVar1531, nVar1532, nVar1533, nVar1534, nVar1535, nVar1536, nVar1537, nVar1538, nVar1539, nVar1540, nVar1541, nVar1542, nVar1543, nVar1544, nVar1545, nVar1546, nVar1547, nVar1548, nVar1549, nVar1550, nVar1551, nVar1552, nVar1553, nVar1554, nVar1555, nVar1556, nVar1557, nVar1558, nVar1559, nVar1560, nVar1561, nVar1562, nVar1563, nVar1564, nVar1565, nVar1566, nVar1567, nVar1568, nVar1569, nVar1570, nVar1571, nVar1572, nVar1573, nVar1574, nVar1575, nVar1576, nVar1577, nVar1578, nVar1579, nVar1580, nVar1581, nVar1582, nVar1583, nVar1584, nVar1585, nVar1586, nVar1587, nVar1588, nVar1589, nVar1590, nVar1591, nVar1592, nVar1593, nVar1594, nVar1595, nVar1596, nVar1597, nVar1598, nVar1599, nVar1600, nVar1601, nVar1602, nVar1603, nVar1604, nVar1605, nVar1606, nVar1607, nVar1608, nVar1609, nVar1610, nVar1611, nVar1612, nVar1613, nVar1614, nVar1615, nVar1616, nVar1617, nVar1618, nVar1619, nVar1620, nVar1621, nVar1622, nVar1623, nVar1624, nVar1625, nVar1626, nVar1627, nVar1628, nVar1629, nVar1630, nVar1631, nVar1632, nVar1633, nVar1634, nVar1635, nVar1636, nVar1637, nVar1638, nVar1639, nVar1640, nVar1641, nVar1642, nVar1643, nVar1644, nVar1645, nVar1646, nVar1647, nVar1648, nVar1649, nVar1650, nVar1651, nVar1652, nVar1653, nVar1654, nVar1655, nVar1656, nVar1657, nVar1658, nVar1659, nVar1660, nVar1661, nVar1662, nVar1663, nVar1664, nVar1665, nVar1666, nVar1667, nVar1668, nVar1669, nVar1670, nVar1671, nVar1672, nVar1673, nVar1674, nVar1675, nVar1676, nVar1677, nVar1678, nVar1679, nVar1680, nVar1681, nVar1682, nVar1683, nVar1684, nVar1685, nVar1686, nVar1687, nVar1688, nVar1689, nVar1690, nVar1691, nVar1692, nVar1693, nVar1694, nVar1695, nVar1696, nVar1697, nVar1698, nVar1699, nVar1700, nVar1701, nVar1702, nVar1703, nVar1704, nVar1705, nVar1706, nVar1707, nVar1708, nVar1709, nVar1710, nVar1711, nVar1712, nVar1713, nVar1714, nVar1715, nVar1716, nVar1717, nVar1718, nVar1719, nVar1720, nVar1721, nVar1722, nVar1723, nVar1724, nVar1725, nVar1726, nVar1727, nVar1728, nVar1729, nVar1730, nVar1731, nVar1732, nVar1733, nVar1734, nVar1735, nVar1736, nVar1737, nVar1738, nVar1739, nVar1740, nVar1741, nVar1742, nVar1743, nVar1744, nVar1745, nVar1746, nVar1747, nVar1748, nVar1749, nVar1750, nVar1751, nVar1752, nVar1753, nVar1754, nVar1755, nVar1756, nVar1757, nVar1758, nVar1759, nVar1760, nVar1761, nVar1762, nVar1763, nVar1764, nVar1765, nVar1766, nVar1767, nVar1768, nVar1769, nVar1770, nVar1771, nVar1772, nVar1773, nVar1774, nVar1775, nVar1776, nVar1777, nVar1778, nVar1779, nVar1780, nVar1781, nVar1782, nVar1783, nVar1784, nVar1785, nVar1786, nVar1787, nVar1788, nVar1789, nVar1790, nVar1791, nVar1792, nVar1793, nVar1794, nVar1795, nVar1796, nVar1797, nVar1798, nVar1799, nVar1800, nVar1801, nVar1802, nVar1803, nVar1804, nVar1805, nVar1806, nVar1807, nVar1808, nVar1809, nVar1810, nVar1811, nVar1812, nVar1813, nVar1814, nVar1815, nVar1816, nVar1817, nVar1818, nVar1819, nVar1820, nVar1821, nVar1822, nVar1823, nVar1824, nVar1825, nVar1826, nVar1827, nVar1828, nVar1829, nVar1830, nVar1831, nVar1832, nVar1833, nVar1834, nVar1835, nVar1836, nVar1837, nVar1838, nVar1839, nVar1840, nVar1841, nVar1842, nVar1843, nVar1844, nVar1845, nVar1846, nVar1847, nVar1848, nVar1849, nVar1850, nVar1851, nVar1852, nVar1853, nVar1854, nVar1855, nVar1856, nVar1857, nVar1858, nVar1859, nVar1860, nVar1861, nVar1862, nVar1863, nVar1864, nVar1865, nVar1866, nVar1867, nVar1868, nVar1869, nVar1870, nVar1871, nVar1872, nVar1873, nVar1874, nVar1875, nVar1876, nVar1877, nVar1878, nVar1879, nVar1880, nVar1881, nVar1882, nVar1883, nVar1884, nVar1885, nVar1886, nVar1887, nVar1888, nVar1889, nVar1890, nVar1891, nVar1892, nVar1893, nVar1894, nVar1895, nVar1896, nVar1897, nVar1898, nVar1899, nVar1900, nVar1901, nVar1902, nVar1903, nVar1904, nVar1905, nVar1906, nVar1907, nVar1908, nVar1909, nVar1910, nVar1911, nVar1912, nVar1913, nVar1914, nVar1915, nVar1916, nVar1917, nVar1918, nVar1919, nVar1920, nVar1921, nVar1922, nVar1923, nVar1924, nVar1925, nVar1926, nVar1928, nVar1929, nVar1930, nVar1931, nVar1932, nVar1933, nVar1934, nVar1935, nVar1936, nVar1937, nVar1938, nVar1939, nVar1940, nVar1941, nVar1942, nVar1943, nVar1944, nVar1945, nVar1946, nVar1947, nVar1948, nVar1949, nVar1950, nVar1951, nVar1952, nVar1953, nVar1954, nVar1955, nVar1956, nVar1957, nVar1958, nVar1959, nVar1960, nVar1961, nVar1962, nVar1963, nVar1964, nVar1965, nVar1966, nVar1967, nVar1968, nVar1969, nVar1970, nVar1971, nVar1972, nVar1973, nVar1974, nVar1975, nVar1976, nVar1977, nVar1978, nVar1979, nVar1980, nVar1981, nVar1982, nVar1983, nVar1984, nVar1985, nVar1986, nVar1987, nVar1988, nVar1989, nVar1990, nVar1991, nVar1992, nVar1993, nVar1994, nVar1995, nVar1996, nVar1997, nVar1998, nVar1999, nVar2000, nVar2001, nVar2002, nVar2003, nVar2004, nVar2005, nVar2006, nVar2007, nVar2008, nVar2009, nVar2010, nVar2011, nVar2012, nVar2013, nVar2014, nVar2015, nVar2016, nVar2017, nVar2018, nVar2019, nVar2020, nVar2021, nVar2022, nVar2023, nVar2024, nVar2025, nVar2026, nVar2027, nVar2028, nVar2029, nVar2030, nVar2031, nVar2032, nVar2033, nVar2034, nVar2035, nVar2036, nVar2037, nVar2038, nVar2039, nVar2040, nVar2041, nVar2042, nVar2043, nVar2044, nVar2045, nVar2046, nVar2047, nVar2048, nVar2049, nVar2050, nVar2051, nVar2052, nVar2053, nVar2054, nVar2055, nVar2056, nVar2057, nVar2058, nVar2059, nVar2060, nVar2061, nVar2062, nVar2063, nVar2064, nVar2065, nVar2066, nVar2067, nVar2068, nVar2069, nVar2070, nVar2071, nVar2072, nVar2073, nVar2074, nVar2075, nVar2076, nVar2077, nVar2078, nVar2079, nVar2080, nVar2081, nVar2082, nVar2083, nVar2084, nVar2085, nVar2086, nVar2087, nVar2088, nVar2089, nVar2090, nVar2091, nVar2092, nVar2093, nVar2094, nVar2095, nVar2096, nVar2097, nVar2098, nVar2099, nVar2100, nVar2101, nVar2102, nVar2104, nVar2105, nVar2106, nVar2107, nVar2108, nVar2109, nVar2110, nVar2111, nVar2112, nVar2113, nVar2114, nVar2115, nVar2116, nVar2117, nVar2118, nVar2119, nVar2120, nVar2121, nVar2122, nVar2123, nVar2124, nVar2125, nVar2126, nVar2127, nVar2128, nVar2129, nVar2130, nVar2131, nVar2132, nVar2133, nVar2134, nVar2135, nVar2136, nVar2137, nVar2138, nVar2139, nVar2140, nVar2141, nVar2142, nVar2143, nVar2144, nVar2145, nVar2146, nVar2147, nVar2148, nVar2149, nVar2150, nVar2151, nVar2152, nVar2153, nVar2154, nVar2155, nVar2156, nVar2157, nVar2158, nVar2159, nVar2160, nVar2161, nVar2162, nVar2163, nVar2164, nVar2165, nVar2166, nVar2167, nVar2168, nVar2169, nVar2170, nVar2171, nVar2172, nVar2173, nVar2174, nVar2175, nVar2176, nVar2177, nVar2178, nVar2180, nVar2181, nVar2182, nVar2183, nVar2184, nVar2185, nVar2186, nVar2187, nVar2188, nVar2189, nVar2190, nVar2191, nVar2192, nVar2193, nVar2194, nVar2195, nVar2196, nVar2197, nVar2198, nVar2199, nVar2200, nVar2201, nVar2202, nVar2203, nVar2204, nVar2205, nVar2206, nVar2207, nVar2208, nVar2209, nVar2210, nVar2211, nVar2212, nVar2213, nVar2214, nVar2215, nVar2216, nVar2217, nVar2218, nVar2219, nVar2220, nVar2221, nVar2222, nVar2223, nVar2224, nVar2225, nVar2226, nVar2227, nVar2228, nVar2229, nVar2230, nVar2231, nVar2232, nVar2233, nVar2234, nVar2235, nVar2236, nVar2237, nVar2238, nVar2239, nVar2240, nVar2241, nVar2242, nVar2243, nVar2244, nVar2245, nVar2246, nVar2247, nVar2248, nVar2249, nVar2250, nVar2251, nVar2252, nVar2253, nVar2254, nVar2255, nVar2256, nVar2257, nVar2258, nVar2259, nVar2260, nVar2261, nVar2262, nVar2263, nVar2264, nVar2265, nVar2266, nVar2267, nVar2268, nVar2269, nVar2270, nVar2271, nVar2272, nVar2273, nVar2274, nVar2275, nVar2276, nVar2277, nVar2278, nVar2279, nVar2280, nVar2281, nVar2282, nVar2283, nVar2284, nVar2285, nVar2286, nVar2287, nVar2288, nVar2289, nVar2290, nVar2291, nVar2292, nVar2293, nVar2294, nVar2295, nVar2296, nVar2297, nVar2298, nVar2299, nVar2300, nVar2301, nVar2302, nVar2303, nVar2304, nVar2305, nVar2306, nVar2307, nVar2308, nVar2309, nVar2310, nVar2311, nVar2312, nVar2313, nVar2314, nVar2315, nVar2316, nVar2317, nVar2318, nVar2319, nVar2320, nVar2321, nVar2322, nVar2323, nVar2324, nVar2325, nVar2326, nVar2327, nVar2328, nVar2329, nVar2330, nVar2331, nVar2332, nVar2333, nVar2334, nVar2335, nVar2336, nVar2337, nVar2338, nVar2339, nVar2340, nVar2341, nVar2342, nVar2343, nVar2344, nVar2345, nVar2346, nVar2347, nVar2348, nVar2349, nVar2350, nVar2351, nVar2352, nVar2353, nVar2354, nVar2355, nVar2356, nVar2357, nVar2358, nVar2359, nVar2360, nVar2361, nVar2362, nVar2363, nVar2364, nVar2365, nVar2366, nVar2367, nVar2368, nVar2369, nVar2370, nVar2371, nVar2372, nVar2373, nVar2374, nVar2375, nVar2376, nVar2377, nVar2378, nVar2379, nVar2380, nVar2381, nVar2382, nVar2383, nVar2384, nVar2385, nVar2386, nVar2387, nVar2388, nVar2389, nVar2390, nVar2391, nVar2392, nVar2393, nVar2394, nVar2395, nVar2396, nVar2397, nVar2398, nVar2399, nVar2400, nVar2401, nVar2402, nVar2403, nVar2404, nVar2405, nVar2406, nVar2407, nVar2408, nVar2409, nVar2410, nVar2411, nVar2412, nVar2413, nVar2414, nVar2415, nVar2416, nVar2417, nVar2418, nVar2419, nVar2420, nVar2421, nVar2422, nVar2423, nVar2424, nVar2425, nVar2426, nVar2427, nVar2428, nVar2429, nVar2430, nVar2431, nVar2432, nVar2433, nVar2434, nVar2435, nVar2436, nVar2437, nVar2438, nVar2439, nVar2440, nVar2441, nVar2442, nVar2443, nVar2444, nVar2445, nVar2446, nVar2447, nVar2448, nVar2449, nVar2450, nVar2451, nVar2452, nVar2453, nVar2454, nVar2455, nVar2456, nVar2457, nVar2458, nVar2459, nVar2460, nVar2461, nVar2462, nVar2463, nVar2464, nVar2465, nVar2466, nVar2467, nVar2468, nVar2469, nVar2470, nVar2471, nVar2472, nVar2473, nVar2474, nVar2475, nVar2476, nVar2477, nVar2478, nVar2479, nVar2480, nVar2481, nVar2482, nVar2483, nVar2484, nVar2485, nVar2486, nVar2487, nVar2488, nVar2489, nVar2490, nVar2491, nVar2492, nVar2493, nVar2494, nVar2495, nVar2496, nVar2497, nVar2498, nVar2499, nVar2500, nVar2501, nVar2502, nVar2503, nVar2504, nVar2505, nVar2506, nVar2507, nVar2508, nVar2509, nVar2510, nVar2511, nVar2512, nVar2513, nVar2514, nVar2515, nVar2516, nVar2517, nVar2518, nVar2519, nVar2520, nVar2521, nVar2522, nVar2523, nVar2524, nVar2525, nVar2526, nVar2527, nVar2528, nVar2529, nVar2530, nVar2531, nVar2532, nVar2533, nVar2534, nVar2535, nVar2536, nVar2537, nVar2538, nVar2539, nVar2540, nVar2541, nVar2542, nVar2543, nVar2544, nVar2545, nVar2546, nVar2547, nVar2548, nVar2549, nVar2550, nVar2551, nVar2552, nVar2553, nVar2554, nVar2555, nVar2556, nVar2557, nVar2558, nVar2559, nVar2560, nVar2561, nVar2562, nVar2563, nVar2564, nVar2565, nVar2566, nVar2567, nVar2568, nVar2569, nVar2570, nVar2571, nVar2572, nVar2573, nVar2574, nVar2575, nVar2576, nVar2577, nVar2578, nVar2579, nVar2580, nVar2581, nVar2582, nVar2583, nVar2584, nVar2585, nVar2586, nVar2587, nVar2588, nVar2589, nVar2590, nVar2591, nVar2592, nVar2593, nVar2594, nVar2595, nVar2596, nVar2597, nVar2598, nVar2599, nVar2600, nVar2601, nVar2602, nVar2603, nVar2604, nVar2605, nVar2606, nVar2607, nVar2608, nVar2609, nVar2610, nVar2611, nVar2612, nVar2613, nVar2614, nVar2615, nVar2616, nVar2617, nVar2618, nVar2619, nVar2620, nVar2622, nVar2623, nVar2624, nVar2625, nVar2626, nVar2627, nVar2628, nVar2629, nVar2630, nVar2631, nVar2633, nVar2634, nVar2635, nVar2636, nVar2637, nVar2638, nVar2639, nVar2640, nVar2641, nVar2642, nVar2643, nVar2644, nVar2645, nVar2646, nVar2647, nVar2648, nVar2649, nVar2650, nVar2651, nVar2652, nVar2653, nVar2654, nVar2655, nVar2656, nVar2657, nVar2658, nVar2659, nVar2660, nVar2661, nVar2662, nVar2663, nVar2664, nVar2665, nVar2666, nVar2667, nVar2668, nVar2669, nVar2670, nVar2671, nVar2672, nVar2673, nVar2674, nVar2675, nVar2676, nVar2677, nVar2678, nVar2679, nVar2680, nVar2681, nVar2682, nVar2683, nVar2684, nVar2685, nVar2686, nVar2687, nVar2688, nVar2689, nVar2690, nVar2691, nVar2692, nVar2693, nVar2694, nVar2695, nVar2696, nVar2697, nVar2698, nVar2699, nVar2700, nVar2701, nVar2702, nVar2703, nVar2704, nVar2705, nVar2706, nVar2707, nVar2708, nVar2709, nVar2710, nVar2711, nVar2712, nVar2713, nVar2714, nVar2715, nVar2716, nVar2717, nVar2718, nVar2719, nVar2720, nVar2721, nVar2722, nVar2723, nVar2724, nVar2725, nVar2726, nVar2727, nVar2728, nVar2729, nVar2730, nVar2731, nVar2732, nVar2733, nVar2734, nVar2735, nVar2736, nVar2737, nVar2738, nVar2739, nVar2740, nVar2741, nVar2742, nVar2743, nVar2744, nVar2745, nVar2746, nVar2747, nVar2748, nVar2749, nVar2750, nVar2751, nVar2752, nVar2753, nVar2755, nVar2756, nVar2757, nVar2758, nVar2759, nVar2760, nVar2761, nVar2762, nVar2763, nVar2764, nVar2765, nVar2766, nVar2767, nVar2768, nVar2769, nVar2770, nVar2771, nVar2772, nVar2773, nVar2774, nVar2775, nVar2776, nVar2777, nVar2778, nVar2779, nVar2780, nVar2781, nVar2782, nVar2783, nVar2784, nVar2785, nVar2786, nVar2787, nVar2788, nVar2789, nVar2790, nVar2791, nVar2792, nVar2793, nVar2794, nVar2795, nVar2796, nVar2797, nVar2798, nVar2799, nVar2800, nVar2801, nVar2802, nVar2803, nVar2804, nVar2805, nVar2806, nVar2807, nVar2808, nVar2809, nVar2810, nVar2811, nVar2812, nVar2813, nVar2814, nVar2815, nVar2816, nVar2817, nVar2818, nVar2819, nVar2820, nVar2821, nVar2822, nVar2823, nVar2824, nVar2825, nVar2826, nVar2827, nVar2828, nVar2829, nVar2830, nVar2831, nVar2832, nVar2833, nVar2834, nVar2835, nVar2836, nVar2837, nVar2838, nVar2839, nVar2840, nVar2841, nVar2842, nVar2843, nVar2844, nVar2845, nVar2846, nVar2847, nVar2848, nVar2849, nVar2850, nVar2851, nVar2852, nVar2853, nVar2854, nVar2855, nVar2856, nVar2857, nVar2858, nVar2859, nVar2860, nVar2861, nVar2862, nVar2863, nVar2864, nVar2865, nVar2866, nVar2867, nVar2868, nVar2869, nVar2870, nVar2871, nVar2872, nVar2873, nVar2874, nVar2875, nVar2876, nVar2877, nVar2878, nVar2879, nVar2880, nVar2881, nVar2882, nVar2883, nVar2884, nVar2885, nVar2886, nVar2887, nVar2888, nVar2889, nVar2890, nVar2891, nVar2892, nVar2893, nVar2894, nVar2895, nVar2896, nVar2897, nVar2898, nVar2899, nVar2900, nVar2901, nVar2902, nVar2903, nVar2904, nVar2905, nVar2906, nVar2907, nVar2908, nVar2909, nVar2910, nVar2911, nVar2912, nVar2913, nVar2914, nVar2915, nVar2916, nVar2917, nVar2918, nVar2919, nVar2920, nVar2921, nVar2922, nVar2923, nVar2924, nVar2925, nVar2926, nVar2927, nVar2928, nVar2929, nVar2930, nVar2931, nVar2932, nVar2933, nVar2934, nVar2935, nVar2936, nVar2937, nVar2938, nVar2939, nVar2940, nVar2941, nVar2942, nVar2943, nVar2944, nVar2945, nVar2946, nVar2947, nVar2948, nVar2949, nVar2950, nVar2951, nVar2952, nVar2953, nVar2954, nVar2955, nVar2956, nVar2957, nVar2958, nVar2959, nVar2960, nVar2961, nVar2962, nVar2963, nVar2964, nVar2965, nVar2966, nVar2967, nVar2968, nVar2969, nVar2970, nVar2971, nVar2972, nVar2973, nVar2974, nVar2975, nVar2976, nVar2977, nVar2978, nVar2979, nVar2980, nVar2981, nVar2982, nVar2983, nVar2984, nVar2985, nVar2986, nVar2987, nVar2988, nVar2989, nVar2990, nVar2991, nVar2992, nVar2993, nVar2994, nVar2995, nVar2996, nVar2997, nVar2998, nVar2999, nVar3000, nVar3001, nVar3002, nVar3003, nVar3004, nVar3005, nVar3006, nVar3007, nVar3008, nVar3009, nVar3010, nVar3011, nVar3012, nVar3013, nVar3014, nVar3015, nVar3016, nVar3017, nVar3018, nVar3019, nVar3020, nVar3021, nVar3022, nVar3023, nVar3024, nVar3025, nVar3026, nVar3027, nVar3028, nVar3029, nVar3030, nVar3031, nVar3032, nVar3033, nVar3034, nVar3035, nVar3036, nVar3037, nVar3038, nVar3039, nVar3040, nVar3041, nVar3042, nVar3043, nVar3044, nVar3045, nVar3046, nVar3047, nVar3049, nVar3050, nVar3051, nVar3052, nVar3053, nVar3054, nVar3055, nVar3056, nVar3057, nVar3058, nVar3059, nVar3060, nVar3061, nVar3063, nVar3064, nVar3065, nVar3066, nVar3067, nVar3068, nVar3069, nVar3070, nVar3071, nVar3072, nVar3073, nVar3074, nVar3075, nVar3076, nVar3077, nVar3078, nVar3079, nVar3080, nVar3081, nVar3082, nVar3083, nVar3084, nVar3085, nVar3086, nVar3087, nVar3088, nVar3089, nVar3090, nVar3091, nVar3092, nVar3093, nVar3094, nVar3095, nVar3096, nVar3097, nVar3098, nVar3099, nVar3100, nVar3101, nVar3102, nVar3103, nVar3104, nVar3105, nVar3106, nVar3107, nVar3108, nVar3109, nVar3110, nVar3111, nVar3112, nVar3113, nVar3114, nVar3115, nVar3116, nVar3117, nVar3118, nVar3119, nVar3120, nVar3121, nVar3122, nVar3123, nVar3124, nVar3125, nVar3126, nVar3127, nVar3128, nVar3129, nVar3130, nVar3131, nVar3132, nVar3133, nVar3134, nVar3135, nVar3136, nVar3137, nVar3138, nVar3140, nVar3141, nVar3142, nVar3143, nVar3144, nVar3145, nVar3146, nVar3147, nVar3148, nVar3149, nVar3150, nVar3151, nVar3152, nVar3153, nVar3154, nVar3155, nVar3156, nVar3157, nVar3158, nVar3159, nVar3160, nVar3161, nVar3162, nVar3163, nVar3164, nVar3165, nVar3166, nVar3167, nVar3168, nVar3169, nVar3170, nVar3171, nVar3172, nVar3173, nVar3174, nVar3175, nVar3176, nVar3177, nVar3178, nVar3179, nVar3180, nVar3181, nVar3182, nVar3183, nVar3184, nVar3185, nVar3186, nVar3187, nVar3188, nVar3189, nVar3190, nVar3191, nVar3192, nVar3193, nVar3194, nVar3195, nVar3196, nVar3197, nVar3198, nVar3199, nVar3200, nVar3201, nVar3202, nVar3203, nVar3204, nVar3205, nVar3206, nVar3207, nVar3208, nVar3209, nVar3210, nVar3211, nVar3212, nVar3213, nVar3214, nVar3215, nVar3216, nVar3217, nVar3218, nVar3219, nVar3220, nVar3221, nVar3222, nVar3223, nVar3224, nVar3225, nVar3226, nVar3227, nVar3228, nVar3229, nVar3230, nVar3231, nVar3232, nVar3233, nVar3234, nVar3235, nVar3236, nVar3237, nVar3238, nVar3239, nVar3240, nVar3241, nVar3242, nVar3243, nVar3244, nVar3245, nVar3246, nVar3247, nVar3248, nVar3249, nVar3250, nVar3251, nVar3252, nVar3253, nVar3254, nVar3255, nVar3256, nVar3257, nVar3258, nVar3259, nVar3260, nVar3261, nVar3262, nVar3263, nVar3264, nVar3265, nVar3266, nVar3267, nVar3268, nVar3269, nVar3270, nVar3271, nVar3272, nVar3273, nVar3274, nVar3275, nVar3276, nVar3277, nVar3278, nVar3279, nVar3280, nVar3281, nVar3282, nVar3283, nVar3284, nVar3285, nVar3286, nVar3287, nVar3288, nVar3289, nVar3290, nVar3291, nVar3292, nVar3293, nVar3294, nVar3295, nVar3296, nVar3297, nVar3298, nVar3299, nVar3300, nVar3301, nVar3302, nVar3303, nVar3304, nVar3305, nVar3306, nVar3307, nVar3308, nVar3309, nVar3310, nVar3311, nVar3312, nVar3313, nVar3314, nVar3315, nVar3316, nVar3317, nVar3318, nVar3319, nVar3320, nVar3321, nVar3322, nVar3323, nVar3324, nVar3325, nVar3326, nVar3327, nVar3328, nVar3329, nVar3330, nVar3331, nVar3332, nVar3333, nVar3334, nVar3335, nVar3336, nVar3337, nVar3338, nVar3339, nVar3340, nVar3341, nVar3342, nVar3343, nVar3344, nVar3345, nVar3346, nVar3347, nVar3348, nVar3349, nVar3350, nVar3351, nVar3352, nVar3353, nVar3354, nVar3355, nVar3356, nVar3357, nVar3358, nVar3359, nVar3360, nVar3361, nVar3362, nVar3363, nVar3364, nVar3365, nVar3366, nVar3367, nVar3368, nVar3369, nVar3370, nVar3371, nVar3372, nVar3373, nVar3374, nVar3375, nVar3376, nVar3377, nVar3378, nVar3379, nVar3380, nVar3381, nVar3382, nVar3383, nVar3384, nVar3385, nVar3386, nVar3387, nVar3388, nVar3389, nVar3390, nVar3391, nVar3392, nVar3393, nVar3394, nVar3395, nVar3396, nVar3397, nVar3398, nVar3399, nVar3400, nVar3401, nVar3402, nVar3403, nVar3404, nVar3405, nVar3406, nVar3407, nVar3408, nVar3409, nVar3410, nVar3411, nVar3412, nVar3413, nVar3414, nVar3415, nVar3416, nVar3417, nVar3418, nVar3419, nVar3420, nVar3421, nVar3422, nVar3423, nVar3424, nVar3425, nVar3426, nVar3427, nVar3428, nVar3429, nVar3430, nVar3431, nVar3432, nVar3433, nVar3434, nVar3435, nVar3436, nVar3437, nVar3438, nVar3439, nVar3440, nVar3441, nVar3442, nVar3443, nVar3444, nVar3445, nVar3446, nVar3447, nVar3448, nVar3449, nVar3450, nVar3451, nVar3452, nVar3453, nVar3454, nVar3455, nVar3456, nVar3457, nVar3458, nVar3459, nVar3460, nVar3461, nVar3462, nVar3463, nVar3464, nVar3465, nVar3466, nVar3467, nVar3468, nVar3469, nVar3470, nVar3471, nVar3472, nVar3473, nVar3474, nVar3475, nVar3476, nVar3477, nVar3478, nVar3479, nVar3480, nVar3481, nVar3482, nVar3483, nVar3484, nVar3485, nVar3486, nVar3487, nVar3488, nVar3489, nVar3490, nVar3491, nVar3492, nVar3493, nVar3494, nVar3495, nVar3496, nVar3497, nVar3498, nVar3499, nVar3500, nVar3501, nVar3502, nVar3503, nVar3504, nVar3505, nVar3506, nVar3507, nVar3508, nVar3509, nVar3510, nVar3511, nVar3512, nVar3513, nVar3514, nVar3515, nVar3516, nVar3517, nVar3518, nVar3519, nVar3520, nVar3521, nVar3522, nVar3523, nVar3524, nVar3525, nVar3526, nVar3527, nVar3528, nVar3529, nVar3530, nVar3531, nVar3532, nVar3533, nVar3534, nVar3535, nVar3536, nVar3537, nVar3538, nVar3539, nVar3540, nVar3541, nVar3542, nVar3543, nVar3544, nVar3545, nVar3546, nVar3547, nVar3548, nVar3549, nVar3550, nVar3551, nVar3552, nVar3553, nVar3554, nVar3555, nVar3556, nVar3557, nVar3558, nVar3559, nVar3560, nVar3561, nVar3562, nVar3563, nVar3564, nVar3565, nVar3566, nVar3567, nVar3568, nVar3569, nVar3570, nVar3571, nVar3572, nVar3573, nVar3574, nVar3575, nVar3576, nVar3577, nVar3578, nVar3579, nVar3580, nVar3581, nVar3582, nVar3583, nVar3584, nVar3585, nVar3586, nVar3587, nVar3588, nVar3589, nVar3590, nVar3591, nVar3592, nVar3593, nVar3594, nVar3595, nVar3596, nVar3597, nVar3598, nVar3599, nVar3600, nVar3601, nVar3602, nVar3603, nVar3604, nVar3605, nVar3606, nVar3607, nVar3608, nVar3609, nVar3610, nVar3611, nVar3612, nVar3613, nVar3614, nVar3615, nVar3616, nVar3617, nVar3618, nVar3619, nVar3620, nVar3621, nVar3622, nVar3623, nVar3624, nVar3625, nVar3626, nVar3627, nVar3628, nVar3629, nVar3630, nVar3631, nVar3632, nVar3633, nVar3634, nVar3635, nVar3636, nVar3637, nVar3638, nVar3639, nVar3640, nVar3641, nVar3642, nVar3643, nVar3644, nVar3645, nVar3646, nVar3647, nVar3648, nVar3649, nVar3650, nVar3651, nVar3652, nVar3653, nVar3654, nVar3655, nVar3656, nVar3657, nVar3658, nVar3659, nVar3660, nVar3661, nVar3662, nVar3663, nVar3664, nVar3665, nVar3666, nVar3667, nVar3668, nVar3669, nVar3670, nVar3671, nVar3672, nVar3673, nVar3674, nVar3675, nVar3676, nVar3677, nVar3678, nVar3679, nVar3680, nVar3681, nVar3682, nVar3683, nVar3684, nVar3685, nVar3686, nVar3687, nVar3688, nVar3689, nVar3690, nVar3691, nVar3692, nVar3693, nVar3694, nVar3695, nVar3696, nVar3697, nVar3698, nVar3699, nVar3700, nVar3701, nVar3702, nVar3703, nVar3704, nVar3705, nVar3706, nVar3707, nVar3708, nVar3709, nVar3710, nVar347, nVar399, nVar1040, nVar1175, nVar2103, nVar2179, nVar2621, nVar2632, nVar2754, nVar3048, nVar3062, nVar3139, nVar3711, nVar3714, nVar3717, nVar3722, nVar3721, nVar1254, nVar280, nVar3718, nVar3719, nVar3720;
diff --git a/Test/symdiff/foo.bpl b/Test/symdiff/foo.bpl index f2c71b8f..85d025d0 100644 --- a/Test/symdiff/foo.bpl +++ b/Test/symdiff/foo.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -z3multipleErrors -errorTrace:0 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -z3multipleErrors -errorTrace:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure Foo(x:int)
{
var ok:bool;
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);
diff --git a/Test/test1/Arrays.bpl b/Test/test1/Arrays.bpl index 9f1d47ba..cb21e4ed 100644 --- a/Test/test1/Arrays.bpl +++ b/Test/test1/Arrays.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 one: [int]int;
var two: [int, int]int;
diff --git a/Test/test1/AssumptionVariables0.bpl b/Test/test1/AssumptionVariables0.bpl index 5cc202b0..7046ea59 100644 --- a/Test/test1/AssumptionVariables0.bpl +++ b/Test/test1/AssumptionVariables0.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 Test0()
{
var {:assumption} a0: bool where a0; // error
diff --git a/Test/test1/AssumptionVariables1.bpl b/Test/test1/AssumptionVariables1.bpl index dea71396..3125650c 100644 --- a/Test/test1/AssumptionVariables1.bpl +++ b/Test/test1/AssumptionVariables1.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 Test0()
{
var {:assumption} a0: int; // error
diff --git a/Test/test1/AttributeTyping.bpl b/Test/test1/AttributeTyping.bpl index d500beca..bcd98feb 100644 --- a/Test/test1/AttributeTyping.bpl +++ b/Test/test1/AttributeTyping.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 {:Incorrect pux0 ++ F0(pux1)} pux0: int;
diff --git a/Test/test1/EmptyCallArgs.bpl b/Test/test1/EmptyCallArgs.bpl index 2df52288..8f5ae31f 100644 --- a/Test/test1/EmptyCallArgs.bpl +++ b/Test/test1/EmptyCallArgs.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;
procedure P(x:int, y:bool) returns (z:C);
diff --git a/Test/test1/Family.bpl b/Test/test1/Family.bpl index 00657658..fec96332 100644 --- a/Test/test1/Family.bpl +++ b/Test/test1/Family.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;
var Heap: <x>[ref,Field x]x;
diff --git a/Test/test1/Frame0.bpl b/Test/test1/Frame0.bpl index 72443d46..6155fc27 100644 --- a/Test/test1/Frame0.bpl +++ b/Test/test1/Frame0.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 g0: int;
var g1: int;
diff --git a/Test/test1/Frame1.bpl b/Test/test1/Frame1.bpl index 23f94488..2ec70270 100644 --- a/Test/test1/Frame1.bpl +++ b/Test/test1/Frame1.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 g0: int;
var g1: int;
diff --git a/Test/test1/FunBody.bpl b/Test/test1/FunBody.bpl index 565b00e5..fc566681 100644 --- a/Test/test1/FunBody.bpl +++ b/Test/test1/FunBody.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 g0<beta>(x:beta) returns (beta);
function g1<beta>() returns (beta);
diff --git a/Test/test1/IfThenElse0.bpl b/Test/test1/IfThenElse0.bpl index 18c58cb2..19918827 100644 --- a/Test/test1/IfThenElse0.bpl +++ b/Test/test1/IfThenElse0.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 foo() { var b:bool, i:int; diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl index c816d05c..962aadf3 100644 --- a/Test/test1/IntReal.bpl +++ b/Test/test1/IntReal.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 i: int;
const r: real;
diff --git a/Test/test1/Lambda.bpl b/Test/test1/Lambda.bpl index 70a61ea8..016bece7 100644 --- a/Test/test1/Lambda.bpl +++ b/Test/test1/Lambda.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 foo() { var a: [int,int]int; diff --git a/Test/test1/LogicalExprs.bpl b/Test/test1/LogicalExprs.bpl index e63e3dce..02174a32 100644 --- a/Test/test1/LogicalExprs.bpl +++ b/Test/test1/LogicalExprs.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 P: bool;
const Q: bool;
diff --git a/Test/test1/MapsTypeErrors.bpl b/Test/test1/MapsTypeErrors.bpl index 135cb7e7..bedb02ec 100644 --- a/Test/test1/MapsTypeErrors.bpl +++ b/Test/test1/MapsTypeErrors.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/test1/Orderings.bpl b/Test/test1/Orderings.bpl index 17d4aea9..4ab28a48 100644 --- a/Test/test1/Orderings.bpl +++ b/Test/test1/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/test1/UpdateExprTyping.bpl b/Test/test1/UpdateExprTyping.bpl index cc1d5e40..bf8fd47c 100644 --- a/Test/test1/UpdateExprTyping.bpl +++ b/Test/test1/UpdateExprTyping.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(a: [int]bool, b: [int]ref, c: [bool]bool)
{
assert a == b; // type error
diff --git a/Test/test1/WhereTyping.bpl b/Test/test1/WhereTyping.bpl index c48590bf..0884e8ef 100644 --- a/Test/test1/WhereTyping.bpl +++ b/Test/test1/WhereTyping.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 g: int where g == 12;
procedure P(x: int where x > 0) returns (y: int where y < 0);
diff --git a/Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl b/Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl index c1bdfa23..1c27c258 100644 --- a/Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl +++ b/Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// simple assert
procedure asserting() {
var x: int;
diff --git a/Test/test15/CaptureState.bpl b/Test/test15/CaptureState.bpl index 5ed6ddcc..113e0b6a 100644 --- a/Test/test15/CaptureState.bpl +++ b/Test/test15/CaptureState.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s -mv:- > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" -mv:- > "%t"
+// RUN: %diff "%s.expect" "%t"
type Ref;
type FieldName;
var Heap: [Ref,FieldName]int;
diff --git a/Test/test15/IntInModel.bpl b/Test/test15/IntInModel.bpl index 68108e5e..55bc14d9 100644 --- a/Test/test15/IntInModel.bpl +++ b/Test/test15/IntInModel.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -printModel:2 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -printModel:2 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure M (i: int) {
assert i != 0;
}
diff --git a/Test/test15/InterpretedFunctionTests.bpl b/Test/test15/InterpretedFunctionTests.bpl index 711a57f3..33db52ef 100644 --- a/Test/test15/InterpretedFunctionTests.bpl +++ b/Test/test15/InterpretedFunctionTests.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure addition(x: int, y: int) {
assume x == 1;
assume y == 2;
diff --git a/Test/test15/ModelTest.bpl b/Test/test15/ModelTest.bpl index 2f03d3c9..7764cb41 100644 --- a/Test/test15/ModelTest.bpl +++ b/Test/test15/ModelTest.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -printModel:2 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -printModel:2 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure M (s : ref, r : ref) {
var i : int, j : int;
i := 0 + 1;
diff --git a/Test/test15/NullInModel.bpl b/Test/test15/NullInModel.bpl index 6bac5c73..aa68b763 100644 --- a/Test/test15/NullInModel.bpl +++ b/Test/test15/NullInModel.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -printModel:2 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -printModel:2 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure M (s: ref) {
assert s != null;
}
diff --git a/Test/test16/LoopUnroll.bpl b/Test/test16/LoopUnroll.bpl index 13841d2c..4ba99eba 100644 --- a/Test/test16/LoopUnroll.bpl +++ b/Test/test16/LoopUnroll.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -loopUnroll:1 -logPrefix:-lu1 LoopUnroll.bpl > %t1
-// RUN: %diff %s.1.expect %t1
-// RUN: %boogie -loopUnroll:2 -logPrefix:-lu2 -proc:ManyIterations LoopUnroll.bpl > %t2
-// RUN: %diff %s.2.expect %t2
-// RUN: %boogie -loopUnroll:3 -logPrefix:-lu3 -proc:ManyIterations LoopUnroll.bpl > %t3
-// RUN: %diff %s.3.expect %t3
+// RUN: %boogie -loopUnroll:1 -logPrefix:-lu1 LoopUnroll.bpl > "%t1"
+// RUN: %diff "%s.1.expect" "%t1"
+// RUN: %boogie -loopUnroll:2 -logPrefix:-lu2 -proc:ManyIterations LoopUnroll.bpl > "%t2"
+// RUN: %diff "%s.2.expect" "%t2"
+// RUN: %boogie -loopUnroll:3 -logPrefix:-lu3 -proc:ManyIterations LoopUnroll.bpl > "%t3"
+// RUN: %diff "%s.3.expect" "%t3"
procedure P()
{
var x: int;
diff --git a/Test/test2/Arrays.bpl b/Test/test2/Arrays.bpl index f153b599..5f4bd9c9 100644 --- a/Test/test2/Arrays.bpl +++ b/Test/test2/Arrays.bpl @@ -1,7 +1,7 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
-// RUN: %boogie -noinfer -typeEncoding:m %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -noinfer -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// -------------------- 1-dimensional arrays --------------------
var A: [ref]int;
diff --git a/Test/test2/AssumeEnsures.bpl b/Test/test2/AssumeEnsures.bpl index 9c19e5bc..74789135 100644 --- a/Test/test2/AssumeEnsures.bpl +++ b/Test/test2/AssumeEnsures.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var g: int;
procedure Foo() returns ();
diff --git a/Test/test2/AssumptionVariables0.bpl b/Test/test2/AssumptionVariables0.bpl index e1800d3d..cc73707c 100644 --- a/Test/test2/AssumptionVariables0.bpl +++ b/Test/test2/AssumptionVariables0.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure Test0()
{
var {:assumption} a0: bool;
diff --git a/Test/test2/Axioms.bpl b/Test/test2/Axioms.bpl index 0da46116..1fa8fab3 100644 --- a/Test/test2/Axioms.bpl +++ b/Test/test2/Axioms.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const Seven: int;
axiom Seven == 7;
diff --git a/Test/test2/B.bpl b/Test/test2/B.bpl index f68dbb26..78f91915 100644 --- a/Test/test2/B.bpl +++ b/Test/test2/B.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// ----------- BEGIN PRELUDE
var Heap: [ref, name]int;
diff --git a/Test/test2/Call.bpl b/Test/test2/Call.bpl index 02902b0a..bf2690cc 100644 --- a/Test/test2/Call.bpl +++ b/Test/test2/Call.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure Bar() returns (barresult: ref);
procedure Foo();
diff --git a/Test/test2/ContractEvaluationOrder.bpl b/Test/test2/ContractEvaluationOrder.bpl index 445b84c6..8719dcfa 100644 --- a/Test/test2/ContractEvaluationOrder.bpl +++ b/Test/test2/ContractEvaluationOrder.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 (x, y: int)
ensures x == y; // ensured by the body
ensures x == 0; // error: not ensured by the body
diff --git a/Test/test2/CutBackEdge.bpl b/Test/test2/CutBackEdge.bpl index c1d08216..2ee7cd68 100644 --- a/Test/test2/CutBackEdge.bpl +++ b/Test/test2/CutBackEdge.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure Test()
{
var i: int;
diff --git a/Test/test2/Ensures.bpl b/Test/test2/Ensures.bpl index 8996d100..c37e31a0 100644 --- a/Test/test2/Ensures.bpl +++ b/Test/test2/Ensures.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var H: [ref,name]int;
var that: ref;
diff --git a/Test/test2/False.bpl b/Test/test2/False.bpl index 5399b024..a0337182 100644 --- a/Test/test2/False.bpl +++ b/Test/test2/False.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure Test1()
{
entry:
diff --git a/Test/test2/FormulaTerm.bpl b/Test/test2/FormulaTerm.bpl index b36f971b..7e762afe 100644 --- a/Test/test2/FormulaTerm.bpl +++ b/Test/test2/FormulaTerm.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Test formula-term distinction in Simplify
procedure plus(x: int, y: int) returns (z: int);
diff --git a/Test/test2/FormulaTerm2.bpl b/Test/test2/FormulaTerm2.bpl index 881a6222..14ae5dab 100644 --- a/Test/test2/FormulaTerm2.bpl +++ b/Test/test2/FormulaTerm2.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// This file has been created to test some of the formula/term issues in Zap.
// However, the test harness does not specify any particular prover to be used,
// since these tests should pass regardless of which prover is used.
diff --git a/Test/test2/FreeCall.bpl b/Test/test2/FreeCall.bpl index aaaba3ac..16f182d9 100644 --- a/Test/test2/FreeCall.bpl +++ b/Test/test2/FreeCall.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Test the implementation of free calls. These calls don't check the preconditions of the
// called procedure in the caller.
diff --git a/Test/test2/IfThenElse1.bpl b/Test/test2/IfThenElse1.bpl index 4c79ce8b..5c12c1f4 100644 --- a/Test/test2/IfThenElse1.bpl +++ b/Test/test2/IfThenElse1.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type t1; procedure ok() diff --git a/Test/test2/Implies.bpl b/Test/test2/Implies.bpl index 05a3e5fe..36c4a134 100644 --- a/Test/test2/Implies.bpl +++ b/Test/test2/Implies.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const a:bool;
const b:bool;
diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl index cbcbd334..ee6c6916 100644 --- a/Test/test2/Lambda.bpl +++ b/Test/test2/Lambda.bpl @@ -1,7 +1,7 @@ -// RUN: %boogie -noinfer %s > %t -// RUN: %diff %s.expect %t -// RUN: %boogie -noinfer -typeEncoding:m %s > %t -// RUN: %diff %s.expect %t +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// RUN: %boogie -noinfer -typeEncoding:m "%s" > "%t" +// RUN: %diff "%s.expect" "%t" procedure foo() { var a: [int]int; diff --git a/Test/test2/LambdaOldExpressions.bpl b/Test/test2/LambdaOldExpressions.bpl index 94a6e520..e865f4ab 100644 --- a/Test/test2/LambdaOldExpressions.bpl +++ b/Test/test2/LambdaOldExpressions.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var b: bool;
diff --git a/Test/test2/LambdaPoly.bpl b/Test/test2/LambdaPoly.bpl index 9a3fa16a..a850d43b 100644 --- a/Test/test2/LambdaPoly.bpl +++ b/Test/test2/LambdaPoly.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type set a = [a]bool; function union<T>(a:set T, b:set T) : set T; axiom (forall<T> a,b:set T :: union(a,b) == (lambda x:T :: a[x] || b[x])); diff --git a/Test/test2/LoopInvAssume.bpl b/Test/test2/LoopInvAssume.bpl index ecbcdc7c..fd95c52e 100644 --- a/Test/test2/LoopInvAssume.bpl +++ b/Test/test2/LoopInvAssume.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Check that assumes in loop invariants are handled correctly
var x : int;
diff --git a/Test/test2/NeverPattern.bpl b/Test/test2/NeverPattern.bpl index c859afe4..aa301129 100644 --- a/Test/test2/NeverPattern.bpl +++ b/Test/test2/NeverPattern.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function {:never_pattern true} f1(x:int) returns(int);
function {:never_pattern false} f2(x:int) returns(int);
function f3(x:int) returns(int);
diff --git a/Test/test2/NullaryMaps.bpl b/Test/test2/NullaryMaps.bpl index ed08ec93..a02f4594 100644 --- a/Test/test2/NullaryMaps.bpl +++ b/Test/test2/NullaryMaps.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// aren't these cool!
var m: []int;
diff --git a/Test/test2/Old.bpl b/Test/test2/Old.bpl index 99db9841..beb98d40 100644 --- a/Test/test2/Old.bpl +++ b/Test/test2/Old.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
var x: int;
var y: int;
diff --git a/Test/test2/OldIllegal.bpl b/Test/test2/OldIllegal.bpl index d2defb25..b9f7bd75 100644 --- a/Test/test2/OldIllegal.bpl +++ b/Test/test2/OldIllegal.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Test old appearing in illegal locations
var Global0: int;
diff --git a/Test/test2/Passification.bpl b/Test/test2/Passification.bpl index 521a9d59..a248ca97 100644 --- a/Test/test2/Passification.bpl +++ b/Test/test2/Passification.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// VC generation tests: passification
procedure good0(x: int) returns (y: int, z: int)
diff --git a/Test/test2/Quantifiers.bpl b/Test/test2/Quantifiers.bpl index e4a50c6b..659a0c47 100644 --- a/Test/test2/Quantifiers.bpl +++ b/Test/test2/Quantifiers.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// ----------------------------------------------------------------------- single trigger
function f(int, int) returns (int);
diff --git a/Test/test2/SelectiveChecking.bpl b/Test/test2/SelectiveChecking.bpl index 16d5bc82..188243c8 100644 --- a/Test/test2/SelectiveChecking.bpl +++ b/Test/test2/SelectiveChecking.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure {:selective_checking} foo() { var x, y, z : int; diff --git a/Test/test2/Structured.bpl b/Test/test2/Structured.bpl index 7a4ad46d..55ee847a 100644 --- a/Test/test2/Structured.bpl +++ b/Test/test2/Structured.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const K: int;
diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl index 51b6655f..6fa379d9 100644 --- a/Test/test2/Timeouts0.bpl +++ b/Test/test2/Timeouts0.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -timeLimit:4 %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -timeLimit:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int)
requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
requires 0 < len;
diff --git a/Test/test2/TypeEncodingM.bpl b/Test/test2/TypeEncodingM.bpl index 8a1bc803..0287da12 100644 --- a/Test/test2/TypeEncodingM.bpl +++ b/Test/test2/TypeEncodingM.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer -typeEncoding:m %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type TT; procedure A() diff --git a/Test/test2/UpdateExpr.bpl b/Test/test2/UpdateExpr.bpl index d89c4715..eb5ba2e1 100644 --- a/Test/test2/UpdateExpr.bpl +++ b/Test/test2/UpdateExpr.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
const a: [int]bool;
diff --git a/Test/test2/Where.bpl b/Test/test2/Where.bpl index 031398ed..fed05d76 100644 --- a/Test/test2/Where.bpl +++ b/Test/test2/Where.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
procedure P0()
{
var x: int where 0 <= x;
diff --git a/Test/test2/sk_hack.bpl b/Test/test2/sk_hack.bpl index 1d902a74..7ce8e4dc 100644 --- a/Test/test2/sk_hack.bpl +++ b/Test/test2/sk_hack.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
function in_set(int) returns(bool);
function next(int) returns(int);
function f(int) returns(bool);
diff --git a/Test/test2/strings-no-where.bpl b/Test/test2/strings-no-where.bpl index e451cc3e..6a89a9b2 100644 --- a/Test/test2/strings-no-where.bpl +++ b/Test/test2/strings-no-where.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type elements;
diff --git a/Test/test2/strings-where.bpl b/Test/test2/strings-where.bpl index 86804051..b2ad7217 100644 --- a/Test/test2/strings-where.bpl +++ b/Test/test2/strings-where.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noinfer %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
type elements;
diff --git a/Test/test20/Coercions.bpl b/Test/test20/Coercions.bpl index 3836332a..0ad114a6 100644 --- a/Test/test20/Coercions.bpl +++ b/Test/test20/Coercions.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, D, E _;
diff --git a/Test/test20/EmptySeq.bpl b/Test/test20/EmptySeq.bpl index b32ca98f..2eeb9589 100644 --- a/Test/test20/EmptySeq.bpl +++ b/Test/test20/EmptySeq.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 Seq T;
function Seq#Length<T>(Seq T) returns (int);
diff --git a/Test/test20/ParallelAssignment.bpl b/Test/test20/ParallelAssignment.bpl index b79d1a10..d84b96ab 100644 --- a/Test/test20/ParallelAssignment.bpl +++ b/Test/test20/ParallelAssignment.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"
// Examples from the Boogie2 language report
// (stuff where resolution succeeds, but typechecking might fail)
diff --git a/Test/test20/ParallelAssignment2.bpl b/Test/test20/ParallelAssignment2.bpl index 0e36bcdd..8f309b75 100644 --- a/Test/test20/ParallelAssignment2.bpl +++ b/Test/test20/ParallelAssignment2.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"
// Examples from the Boogie2 language report
// (examples where already resolution fails)
diff --git a/Test/test20/PolyFuns0.bpl b/Test/test20/PolyFuns0.bpl index 0df74e15..c7d44b9f 100644 --- a/Test/test20/PolyFuns0.bpl +++ b/Test/test20/PolyFuns0.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 size<alpha>(x : alpha) returns (int);
diff --git a/Test/test20/PolyFuns1.bpl b/Test/test20/PolyFuns1.bpl index cc38b720..12a8a1b8 100644 --- a/Test/test20/PolyFuns1.bpl +++ b/Test/test20/PolyFuns1.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<a>( <b>[b]a ) returns (bool);
const M: <a>[ <b>[b]a ] bool;
diff --git a/Test/test20/PolyPolyPoly.bpl b/Test/test20/PolyPolyPoly.bpl index e45a24be..718452f2 100644 --- a/Test/test20/PolyPolyPoly.bpl +++ b/Test/test20/PolyPolyPoly.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/test20/PolyPolyPoly2.bpl b/Test/test20/PolyPolyPoly2.bpl index b9249553..e50251c1 100644 --- a/Test/test20/PolyPolyPoly2.bpl +++ b/Test/test20/PolyPolyPoly2.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 p: <a>[]a;
const q: <a,b>[a]b;
diff --git a/Test/test20/PolyProcs0.bpl b/Test/test20/PolyProcs0.bpl index 4867614a..698e2f12 100644 --- a/Test/test20/PolyProcs0.bpl +++ b/Test/test20/PolyProcs0.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 Field a;
diff --git a/Test/test20/ProcParamReordering.bpl b/Test/test20/ProcParamReordering.bpl index f88aaea5..2532964f 100644 --- a/Test/test20/ProcParamReordering.bpl +++ b/Test/test20/ProcParamReordering.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/test20/Prog0.bpl b/Test/test20/Prog0.bpl index 2aa974c5..26642737 100644 --- a/Test/test20/Prog0.bpl +++ b/Test/test20/Prog0.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"
// Let's test some Boogie 2 features ...
type elements;
diff --git a/Test/test20/Prog1.bpl b/Test/test20/Prog1.bpl index cdc88779..7fcf91b6 100644 --- a/Test/test20/Prog1.bpl +++ b/Test/test20/Prog1.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"
// Let's test some Boogie 2 features ...
type elements;
diff --git a/Test/test20/Prog2.bpl b/Test/test20/Prog2.bpl index c186eafc..79555d28 100644 --- a/Test/test20/Prog2.bpl +++ b/Test/test20/Prog2.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 union(<a> [a] bool, <a> [a] bool) returns (<a> [a] bool);
axiom (forall<alpha> // error: alpha has to occur in dummy types
diff --git a/Test/test20/TypeDecls0.bpl b/Test/test20/TypeDecls0.bpl index cb4dc1d3..a78008c2 100644 --- a/Test/test20/TypeDecls0.bpl +++ b/Test/test20/TypeDecls0.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 a _ b;
type D;
type E _;
diff --git a/Test/test20/TypeDecls1.bpl b/Test/test20/TypeDecls1.bpl index 7b64cd5b..52f28e06 100644 --- a/Test/test20/TypeDecls1.bpl +++ b/Test/test20/TypeDecls1.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"
// set of maps from anything to a specific type a
const mapSet : <a>[<b>[b]a]bool;
diff --git a/Test/test20/TypeSynonyms0.bpl b/Test/test20/TypeSynonyms0.bpl index f43366f2..1703f4a7 100644 --- a/Test/test20/TypeSynonyms0.bpl +++ b/Test/test20/TypeSynonyms0.bpl @@ -1,7 +1,7 @@ -// RUN: %boogie -noVerify %s > %t
-// RUN: %diff %s.expect %t
-// RUN: %boogie -noVerify -print:- -env:0 %s > %t
-// RUN: %diff %s.print.expect %t
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t"
+// RUN: %diff "%s.print.expect" "%t"
type Set a = [a]bool;
diff --git a/Test/test20/TypeSynonyms1.bpl b/Test/test20/TypeSynonyms1.bpl index 890f494f..98ecedca 100644 --- a/Test/test20/TypeSynonyms1.bpl +++ b/Test/test20/TypeSynonyms1.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"
diff --git a/Test/test20/TypeSynonyms2.bpl b/Test/test20/TypeSynonyms2.bpl index 90450c2a..472b1e96 100644 --- a/Test/test20/TypeSynonyms2.bpl +++ b/Test/test20/TypeSynonyms2.bpl @@ -1,7 +1,7 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
-// RUN: %boogie -noVerify -print:- -env:0 -printDesugared %s > %t
-// RUN: %diff %s.print.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -noVerify -print:- -env:0 -printDesugared "%s" > "%t"
+// RUN: %diff "%s.print.expect" "%t"
type Set a = [a]bool;
diff --git a/Test/test21/BooleanQuantification.bpl b/Test/test21/BooleanQuantification.bpl index 527ab174..1493269b 100644 --- a/Test/test21/BooleanQuantification.bpl +++ b/Test/test21/BooleanQuantification.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
diff --git a/Test/test21/BooleanQuantification2.bpl b/Test/test21/BooleanQuantification2.bpl index 73234024..22dfd217 100644 --- a/Test/test21/BooleanQuantification2.bpl +++ b/Test/test21/BooleanQuantification2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
axiom (forall x:bool :: x || !x);
diff --git a/Test/test21/Boxing.bpl b/Test/test21/Boxing.bpl index 00e3013e..0112b6cf 100644 --- a/Test/test21/Boxing.bpl +++ b/Test/test21/Boxing.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type Box;
diff --git a/Test/test21/Casts.bpl b/Test/test21/Casts.bpl index 1320cff2..739185ea 100644 --- a/Test/test21/Casts.bpl +++ b/Test/test21/Casts.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
procedure P() returns () {
diff --git a/Test/test21/Coercions2.bpl b/Test/test21/Coercions2.bpl index 849376f5..e9a78574 100644 --- a/Test/test21/Coercions2.bpl +++ b/Test/test21/Coercions2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type Box, C;
diff --git a/Test/test21/Colors.bpl b/Test/test21/Colors.bpl index 7e63c9ff..f0e12672 100644 --- a/Test/test21/Colors.bpl +++ b/Test/test21/Colors.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type Color;
diff --git a/Test/test21/DisjointDomains.bpl b/Test/test21/DisjointDomains.bpl index 303d0e4f..30d8a6f7 100644 --- a/Test/test21/DisjointDomains.bpl +++ b/Test/test21/DisjointDomains.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type C _;
function f<a>(C a) returns (int);
diff --git a/Test/test21/DisjointDomains2.bpl b/Test/test21/DisjointDomains2.bpl index 8677d9dc..ae25a20e 100644 --- a/Test/test21/DisjointDomains2.bpl +++ b/Test/test21/DisjointDomains2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type C _;
function f<a>(C a) returns (int);
diff --git a/Test/test21/EmptyList.bpl b/Test/test21/EmptyList.bpl index 28362b73..450cd064 100644 --- a/Test/test21/EmptyList.bpl +++ b/Test/test21/EmptyList.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type List _;
diff --git a/Test/test21/EmptySetBug.bpl b/Test/test21/EmptySetBug.bpl index 06a42652..e3feb16c 100644 --- a/Test/test21/EmptySetBug.bpl +++ b/Test/test21/EmptySetBug.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type ref;
const null: ref;
diff --git a/Test/test21/Flattening.bpl b/Test/test21/Flattening.bpl index 4ef7e5c8..ddebd9ab 100644 --- a/Test/test21/Flattening.bpl +++ b/Test/test21/Flattening.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
function g(int) returns (int);
diff --git a/Test/test21/FunAxioms.bpl b/Test/test21/FunAxioms.bpl index c51024ad..5964b4e8 100644 --- a/Test/test21/FunAxioms.bpl +++ b/Test/test21/FunAxioms.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type Pair a b;
diff --git a/Test/test21/FunAxioms2.bpl b/Test/test21/FunAxioms2.bpl index 3b9bccf2..6e087baf 100644 --- a/Test/test21/FunAxioms2.bpl +++ b/Test/test21/FunAxioms2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type T;
diff --git a/Test/test21/HeapAbstraction.bpl b/Test/test21/HeapAbstraction.bpl index 6f88189c..0fb2f007 100644 --- a/Test/test21/HeapAbstraction.bpl +++ b/Test/test21/HeapAbstraction.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type Field a, Heap = <a>[ref, Field a]a;
diff --git a/Test/test21/HeapAxiom.bpl b/Test/test21/HeapAxiom.bpl index adb3f632..691c97f9 100644 --- a/Test/test21/HeapAxiom.bpl +++ b/Test/test21/HeapAxiom.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type Field a, Heap = <a>[ref, Field a]a;
diff --git a/Test/test21/InterestingExamples0.bpl b/Test/test21/InterestingExamples0.bpl index d3021553..08ed61d4 100644 --- a/Test/test21/InterestingExamples0.bpl +++ b/Test/test21/InterestingExamples0.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
procedure P() returns () {
var a : <t>[t]int;
diff --git a/Test/test21/InterestingExamples1.bpl b/Test/test21/InterestingExamples1.bpl index a530c625..247e2c5b 100644 --- a/Test/test21/InterestingExamples1.bpl +++ b/Test/test21/InterestingExamples1.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type Set = <a> [a] bool;
type Field a;
diff --git a/Test/test21/InterestingExamples2.bpl b/Test/test21/InterestingExamples2.bpl index fd17b122..6fc8d259 100644 --- a/Test/test21/InterestingExamples2.bpl +++ b/Test/test21/InterestingExamples2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
procedure P() returns () {
diff --git a/Test/test21/InterestingExamples3.bpl b/Test/test21/InterestingExamples3.bpl index 3acca9a1..24e89b2b 100644 --- a/Test/test21/InterestingExamples3.bpl +++ b/Test/test21/InterestingExamples3.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
procedure P() returns () {
diff --git a/Test/test21/InterestingExamples4.bpl b/Test/test21/InterestingExamples4.bpl index db2e9682..941c9020 100644 --- a/Test/test21/InterestingExamples4.bpl +++ b/Test/test21/InterestingExamples4.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
// a property that should hold according to the Boogie semantics
// (but no automatic theorem prover will be able to prove it)
diff --git a/Test/test21/InterestingExamples5.bpl b/Test/test21/InterestingExamples5.bpl index be388839..3f4e4f34 100644 --- a/Test/test21/InterestingExamples5.bpl +++ b/Test/test21/InterestingExamples5.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type C a;
diff --git a/Test/test21/Keywords.bpl b/Test/test21/Keywords.bpl index 9af526e4..3be91fa8 100644 --- a/Test/test21/Keywords.bpl +++ b/Test/test21/Keywords.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
function NOT(x:int) returns(int);
diff --git a/Test/test21/LargeLiterals0.bpl b/Test/test21/LargeLiterals0.bpl index 203e9bc5..57877f9d 100644 --- a/Test/test21/LargeLiterals0.bpl +++ b/Test/test21/LargeLiterals0.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
var x : int;
diff --git a/Test/test21/LetSorting.bpl b/Test/test21/LetSorting.bpl index 38e77396..c58c6242 100644 --- a/Test/test21/LetSorting.bpl +++ b/Test/test21/LetSorting.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
procedure Array0() returns (z: int)
diff --git a/Test/test21/MapAxiomsConsistency.bpl b/Test/test21/MapAxiomsConsistency.bpl index 66e7a142..4c8302a4 100644 --- a/Test/test21/MapAxiomsConsistency.bpl +++ b/Test/test21/MapAxiomsConsistency.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
// Dafny program verifier version 0.92, Copyright (c) 2003-2008, Microsoft.
// Command Line Options: /trace /typeEncoding:arguments /print:test.bpl test.dfy
diff --git a/Test/test21/MapOutputTypeParams.bpl b/Test/test21/MapOutputTypeParams.bpl index 4e83e6f1..c9304d34 100644 --- a/Test/test21/MapOutputTypeParams.bpl +++ b/Test/test21/MapOutputTypeParams.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
diff --git a/Test/test21/Maps0.bpl b/Test/test21/Maps0.bpl index ba3a0f98..125730ef 100644 --- a/Test/test21/Maps0.bpl +++ b/Test/test21/Maps0.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
const a : [int] bool;
diff --git a/Test/test21/Maps1.bpl b/Test/test21/Maps1.bpl index 417521eb..024cd50f 100644 --- a/Test/test21/Maps1.bpl +++ b/Test/test21/Maps1.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
// different map type classes with the same arity
diff --git a/Test/test21/Maps2.bpl b/Test/test21/Maps2.bpl index ea020afd..0b7980c7 100644 --- a/Test/test21/Maps2.bpl +++ b/Test/test21/Maps2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
// XFAIL: *
type T;
diff --git a/Test/test21/NameClash.bpl b/Test/test21/NameClash.bpl index 9b6fefa8..d31a6e01 100644 --- a/Test/test21/NameClash.bpl +++ b/Test/test21/NameClash.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
function f(int) returns (int);
diff --git a/Test/test21/Orderings.bpl b/Test/test21/Orderings.bpl index 6a048224..39361461 100644 --- a/Test/test21/Orderings.bpl +++ b/Test/test21/Orderings.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
const a, b:int;
diff --git a/Test/test21/Orderings2.bpl b/Test/test21/Orderings2.bpl index fe01184c..01d3be15 100644 --- a/Test/test21/Orderings2.bpl +++ b/Test/test21/Orderings2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
const b:int;
diff --git a/Test/test21/Orderings3.bpl b/Test/test21/Orderings3.bpl index a842be12..3036d8e6 100644 --- a/Test/test21/Orderings3.bpl +++ b/Test/test21/Orderings3.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
// Example from the Boogie 2 language report
diff --git a/Test/test21/Orderings4.bpl b/Test/test21/Orderings4.bpl index 62f7b7fa..00da92dc 100644 --- a/Test/test21/Orderings4.bpl +++ b/Test/test21/Orderings4.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
type Wicket;
diff --git a/Test/test21/ParallelAssignment.bpl b/Test/test21/ParallelAssignment.bpl index 6bd414e9..6f7c7639 100644 --- a/Test/test21/ParallelAssignment.bpl +++ b/Test/test21/ParallelAssignment.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
// Examples from the Boogie2 language report
type C, D;
diff --git a/Test/test21/PolyList.bpl b/Test/test21/PolyList.bpl index c68c637e..08fcd637 100644 --- a/Test/test21/PolyList.bpl +++ b/Test/test21/PolyList.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl index 42b1f889..eb140f77 100644 --- a/Test/test21/Real.bpl +++ b/Test/test21/Real.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
axiom (forall r: real :: r == 0.0 || r / r == 1.0);
procedure P(a: real, b: real) returns () {
diff --git a/Test/test21/Triggers0.bpl b/Test/test21/Triggers0.bpl index f58b168f..c3ff14d5 100644 --- a/Test/test21/Triggers0.bpl +++ b/Test/test21/Triggers0.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
const ar : [int]bool;
diff --git a/Test/test21/Triggers1.bpl b/Test/test21/Triggers1.bpl index 63a780f5..a4199040 100644 --- a/Test/test21/Triggers1.bpl +++ b/Test/test21/Triggers1.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
diff --git a/Test/test21/test3_AddMethod_conv.bpl b/Test/test21/test3_AddMethod_conv.bpl index d0abb5c3..89c34c45 100644 --- a/Test/test21/test3_AddMethod_conv.bpl +++ b/Test/test21/test3_AddMethod_conv.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
-// RUN: %diff %s.n.expect %t
-// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
-// RUN: %diff %s.p.expect %t
-// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
-// RUN: %diff %s.a.expect %t
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
+// RUN: %diff "%s.n.expect" "%t"
+// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %diff "%s.p.expect" "%t"
+// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+// RUN: %diff "%s.a.expect" "%t"
// XFAIL: *
// Spec# program verifier version 0.90, Copyright (c) 2003-2008, Microsoft.
// Command Line Options: /print:debug.txt AddMethod.dll
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
diff --git a/Test/textbook/BQueue.bpl b/Test/textbook/BQueue.bpl index 1c52a0e8..f224334c 100644 --- a/Test/textbook/BQueue.bpl +++ b/Test/textbook/BQueue.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// BQueue.bpl
// A queue program specified in the style of dynamic frames.
// Rustan Leino, Michal Moskal, and Wolfram Schulte, 2007.
diff --git a/Test/textbook/Bubble.bpl b/Test/textbook/Bubble.bpl index 937ab7e5..702b2cc9 100644 --- a/Test/textbook/Bubble.bpl +++ b/Test/textbook/Bubble.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Bubble Sort, where the specification says the output is a permutation of
// the input.
diff --git a/Test/textbook/DivMod.bpl b/Test/textbook/DivMod.bpl index de218604..bdbc4f19 100644 --- a/Test/textbook/DivMod.bpl +++ b/Test/textbook/DivMod.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 contains two definitions of integer div/mod (truncated division, as is
// used in C, C#, Java, and several other languages, and Euclidean division, which
// has mathematical appeal and is used by SMT Lib) and proves the correct
diff --git a/Test/textbook/DutchFlag.bpl b/Test/textbook/DutchFlag.bpl index 64743303..8bac6aec 100644 --- a/Test/textbook/DutchFlag.bpl +++ b/Test/textbook/DutchFlag.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// The partition step of Quick Sort picks a 'pivot' element from a specified subsection
// of a given integer array. It then partially sorts the elements of the array so that
// elements smaller than the pivot end up to the left of the pivot and elements larger
diff --git a/Test/textbook/Find.bpl b/Test/textbook/Find.bpl index 2b149baf..5a77c621 100644 --- a/Test/textbook/Find.bpl +++ b/Test/textbook/Find.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// Declare a constant 'K' and a function 'f' and postulate that 'K' is
// in the image of 'f'
const K: int;
diff --git a/Test/textbook/McCarthy-91.bpl b/Test/textbook/McCarthy-91.bpl index 895c8e8c..6bfbcb04 100644 --- a/Test/textbook/McCarthy-91.bpl +++ b/Test/textbook/McCarthy-91.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// McCarthy 91 function
procedure F(n: int) returns (r: int)
ensures 100 < n ==> r == n - 10;
diff --git a/Test/textbook/TuringFactorial.bpl b/Test/textbook/TuringFactorial.bpl index d0c40e84..dffc36ab 100644 --- a/Test/textbook/TuringFactorial.bpl +++ b/Test/textbook/TuringFactorial.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie %s > %t
-// RUN: %diff %s.expect %t
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
// A Boogie version of Turing's additive factorial program, from "Checking a large routine"
// published in the "Report of a Conference of High Speed Automatic Calculating Machines",
// pp. 67-69, 1949.
|