summaryrefslogtreecommitdiff
path: root/Test/inline
diff options
context:
space:
mode:
Diffstat (limited to 'Test/inline')
-rw-r--r--Test/inline/Elevator.bpl6
-rw-r--r--Test/inline/InliningAndLoops.bpl4
-rw-r--r--Test/inline/codeexpr.bpl4
-rw-r--r--Test/inline/expansion2.bpl6
-rw-r--r--Test/inline/expansion3.bpl4
-rw-r--r--Test/inline/expansion4.bpl4
-rw-r--r--Test/inline/fundef.bpl4
-rw-r--r--Test/inline/fundef2.bpl4
-rw-r--r--Test/inline/polyInline.bpl6
-rw-r--r--Test/inline/test0.bpl4
-rw-r--r--Test/inline/test1.bpl4
-rw-r--r--Test/inline/test2.bpl4
-rw-r--r--Test/inline/test3.bpl4
-rw-r--r--Test/inline/test4.bpl4
-rw-r--r--Test/inline/test5.bpl4
-rw-r--r--Test/inline/test6.bpl4
16 files changed, 35 insertions, 35 deletions
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;
{
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 07:03:22 +0000