diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-27 20:53:49 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-27 20:53:49 +0100 |
| commit | 02aca9ffab2d5a63e89f83d5eadb7133132c3b0a (patch) | |
| tree | 673526b54101f72b42813d6f05edaba15f82b727 /Test/AbsHoudini | |
| parent | 75416c24e78d9992c10fbb86ba458e813acf943d (diff) | |
Fix lit test suite when running Boogie under a path that contains
spaces.
Diffstat (limited to 'Test/AbsHoudini')
28 files changed, 56 insertions, 56 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;
|