summaryrefslogtreecommitdiff
path: root/Test/houdini
diff options
context:
space:
mode:
Diffstat (limited to 'Test/houdini')
-rw-r--r--Test/houdini/houd1.bpl4
-rw-r--r--Test/houdini/houd10.bpl4
-rw-r--r--Test/houdini/houd11.bpl4
-rw-r--r--Test/houdini/houd12.bpl2
-rw-r--r--Test/houdini/houd2.bpl4
-rw-r--r--Test/houdini/houd3.bpl4
-rw-r--r--Test/houdini/houd4.bpl4
-rw-r--r--Test/houdini/houd5.bpl4
-rw-r--r--Test/houdini/houd6.bpl4
-rw-r--r--Test/houdini/houd7.bpl4
-rw-r--r--Test/houdini/houd8.bpl4
-rw-r--r--Test/houdini/houd9.bpl4
-rw-r--r--Test/houdini/test1.bpl4
-rw-r--r--Test/houdini/test10.bpl4
-rw-r--r--Test/houdini/test2.bpl4
-rw-r--r--Test/houdini/test7.bpl4
-rw-r--r--Test/houdini/test8.bpl4
-rw-r--r--Test/houdini/test9.bpl4
18 files changed, 35 insertions, 35 deletions
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;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 23:53:09 +0000