diff options
Diffstat (limited to 'Test/test0/MapsResolutionErrors.bpl')
-rw-r--r-- | Test/test0/MapsResolutionErrors.bpl | 60 |
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() } |