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.

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;