summaryrefslogtreecommitdiff
path: root/Test/test1
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test1')
-rw-r--r--Test/test1/Arrays.bpl4
-rw-r--r--Test/test1/AssumptionVariables0.bpl4
-rw-r--r--Test/test1/AssumptionVariables1.bpl4
-rw-r--r--Test/test1/AttributeTyping.bpl4
-rw-r--r--Test/test1/EmptyCallArgs.bpl4
-rw-r--r--Test/test1/Family.bpl4
-rw-r--r--Test/test1/Frame0.bpl4
-rw-r--r--Test/test1/Frame1.bpl4
-rw-r--r--Test/test1/FunBody.bpl4
-rw-r--r--Test/test1/IfThenElse0.bpl4
-rw-r--r--Test/test1/IntReal.bpl4
-rw-r--r--Test/test1/Lambda.bpl4
-rw-r--r--Test/test1/LogicalExprs.bpl4
-rw-r--r--Test/test1/MapsTypeErrors.bpl4
-rw-r--r--Test/test1/Orderings.bpl4
-rw-r--r--Test/test1/UpdateExprTyping.bpl4
-rw-r--r--Test/test1/WhereTyping.bpl4
17 files changed, 34 insertions, 34 deletions
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);
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 02:17:01 +0000