diff options
author | MichalMoskal <unknown> | 2009-12-17 01:17:59 +0000 |
---|---|---|
committer | MichalMoskal <unknown> | 2009-12-17 01:17:59 +0000 |
commit | 9447617aefbe9706b0d74a827181976e4b9e9d26 (patch) | |
tree | 471ea6938e90be46af5e6ce8e7ca88de1081c977 /Test/test21/MapAxiomsConsistency.bpl | |
parent | fa8cb4c335668f180fa2c181ca6bb1ad87b54c4a (diff) |
Allow ":" in addition to "returns" in function definitions. Make the pretty-printer use ":" not "returns".
Allow foo(x,y,z:int,p,q:ptr) kind of syntax in function definitions.
Consequently foo(int,y:bool) is no longer allowed.
Update the testsuite to match that.
Diffstat (limited to 'Test/test21/MapAxiomsConsistency.bpl')
-rw-r--r-- | Test/test21/MapAxiomsConsistency.bpl | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/test21/MapAxiomsConsistency.bpl b/Test/test21/MapAxiomsConsistency.bpl index d5344449..a27f89c4 100644 --- a/Test/test21/MapAxiomsConsistency.bpl +++ b/Test/test21/MapAxiomsConsistency.bpl @@ -26,8 +26,8 @@ function Seq#Index<T>(Seq T, int) returns (T); function Seq#Contains<T>(Seq T, T) returns (bool);
function Seq#Equal<T>(Seq T, Seq T) returns (bool);
function Seq#SameUntil<T>(Seq T, Seq T, int) returns (bool);
-function Seq#Take<T>(Seq T, howMany: int) returns (Seq T);
-function Seq#Drop<T>(Seq T, howMany: int) returns (Seq T);
+function Seq#Take<T>(s:Seq T, howMany: int) returns (Seq T);
+function Seq#Drop<T>(s:Seq T, howMany: int) returns (Seq T);
type Field _;
type HeapType = <alpha>[ref,Field alpha]alpha;
|