summaryrefslogtreecommitdiff
path: root/Test/test0/MapsResolutionErrors.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test0/MapsResolutionErrors.bpl')
-rw-r--r--Test/test0/MapsResolutionErrors.bpl60
1 files changed, 30 insertions, 30 deletions
diff --git a/Test/test0/MapsResolutionErrors.bpl b/Test/test0/MapsResolutionErrors.bpl
index 4cd5ff19..204cb7b0 100644
--- a/Test/test0/MapsResolutionErrors.bpl
+++ b/Test/test0/MapsResolutionErrors.bpl
@@ -1,30 +1,30 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-var m: []int;
-var p: <a>[]a;
-
-type C _;
-var bad: <a,b>[]C a; // error: b is not used
-
-function F<a>(a, int) returns (bool) { true }
-
-type Set _;
-function EmptySet<a>() returns (Set a);
-function G<a>(a, int) returns (Set a) { EmptySet() }
-
-function H<a>(int) returns (Set a);
-
-function {:inline true} K<a>(int) returns (Set a)
-{ EmptySet() }
-
-
-procedure P<a>(x: int, y: bool) returns (z: int, w: bool); // error: "a" is not used
-
-procedure Q<a>(x: int, y: bool) returns (z: int, w: a);
-procedure R<a>(x: int, y: bool) returns (z: int, w: Set a);
-procedure S<a>(x: a, y: bool) returns (z: int, w: Set a);
-
-
-function K2<a>(int) returns (Set a) // now ok
-{ EmptySet() }
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var m: []int;
+var p: <a>[]a;
+
+type C _;
+var bad: <a,b>[]C a; // error: b is not used
+
+function F<a>(a, int) returns (bool) { true }
+
+type Set _;
+function EmptySet<a>() returns (Set a);
+function G<a>(a, int) returns (Set a) { EmptySet() }
+
+function H<a>(int) returns (Set a);
+
+function {:inline true} K<a>(int) returns (Set a)
+{ EmptySet() }
+
+
+procedure P<a>(x: int, y: bool) returns (z: int, w: bool); // error: "a" is not used
+
+procedure Q<a>(x: int, y: bool) returns (z: int, w: a);
+procedure R<a>(x: int, y: bool) returns (z: int, w: Set a);
+procedure S<a>(x: a, y: bool) returns (z: int, w: Set a);
+
+
+function K2<a>(int) returns (Set a) // now ok
+{ EmptySet() }