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.

7 files changed, 22 insertions, 20 deletions

diff --git a/Test/inline/Answer b/Test/inline/Answer
index 854ac558..c59772cd 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -953,17 +953,17 @@ Boogie program verifier finished with 1 verified, 0 errors
 Boogie program verifier finished with 3 verified, 0 errors

 -------------------- fundef.bpl --------------------

 

-function {:inline true} foo(x: int) returns (bool)

+function {:inline true} foo(x: int) : bool

 {

   x > 0

 }

 

-function {:inline false} foo2(x: int) returns (bool);

+function {:inline false} foo2(x: int) : bool;

 

 // autogenerated definition axiom

 axiom (forall x: int :: {:inline false} { foo2(x): bool } foo2(x): bool == (x > 0));

 

-function foo3(x: int) returns (bool);

+function foo3(x: int) : bool;

 

 // autogenerated definition axiom

 axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));

diff --git a/Test/test0/Answer b/Test/test0/Answer
index e8ea231e..90721188 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -76,7 +76,7 @@ axiom P || Q || Q || R;
 

 axiom P && Q && Q && R;

 

-function f(int) returns (int);

+function f(int) : int;

 

 axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x + x) } { f(x) * f(x) } {:nopats f(x + x + x) } f(f(x)) < 200);

 

@@ -87,10 +87,12 @@ Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in t
 Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q

 2 type checking errors detected in Arrays1.bpl

 Types0.bpl(6,18): Error: expected identifier before ':'

-1 parse errors detected in Types0.bpl

+Types0.bpl(6,12): Error: expecting an identifier as parameter name

+2 parse errors detected in Types0.bpl

 Types1.bpl(6,11): Error: undeclared type: x

-Types1.bpl(7,18): Error: undeclared type: x

-2 name resolution errors detected in Types1.bpl

+Types1.bpl(7,11): Error: undeclared type: x

+Types1.bpl(7,14): Error: undeclared type: x

+3 name resolution errors detected in Types1.bpl

 WhereParsing.bpl(14,37): Error: where clause not allowed here

 WhereParsing.bpl(15,33): Error: where clause not allowed here

 2 parse errors detected in WhereParsing.bpl

@@ -153,7 +155,7 @@ AttributeParsingErr.bpl(20,26): Error: only attributes, not triggers, allowed he
 

 type {:sourcefile "test.ssc"} T;

 

-function {:source "test.scc"} f(int) returns (int);

+function {:source "test.scc"} f(int) : int;

 

 const {:description "The largest integer value"} unique MAXINT: int;

 

@@ -201,7 +203,7 @@ AttributeResolution.bpl(9,18): Error: undeclared identifier: mux
 AttributeResolution.bpl(11,29): Error: undeclared identifier: fux

 9 name resolution errors detected in AttributeResolution.bpl

 

-function \true() returns (bool);

+function \true() : bool;

 

 type \procedure;

 

diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl
index 09edbd12..cb69aa5f 100644
--- a/Test/test0/ModifiedBag.bpl
+++ b/Test/test0/ModifiedBag.bpl
@@ -41,19 +41,19 @@ function $RefArraySet(elements, int, ref) returns (elements);
 

 function $IntArrayGet(elements, int) returns (value: int);

 

-function $IntArraySet(elements, int, value: int) returns (elements);

+function $IntArraySet(elements, int, int) returns (elements);

 

 function $RealArrayGet(elements, int) returns (value: real);

 

-function $RealArraySet(elements, int, value: real) returns (elements);

+function $RealArraySet(elements, int, real) returns (elements);

 

 function $BoolArrayGet(elements, int) returns (value: bool);

 

-function $BoolArraySet(elements, int, value: bool) returns (elements);

+function $BoolArraySet(elements, int, bool) returns (elements);

 

 function $ArrayArrayGet(elements, int) returns (value: elements);

 

-function $ArrayArraySet(elements, int, value: elements) returns (elements);

+function $ArrayArraySet(elements, int, elements) returns (elements);

 

 axiom (forall A: elements, i: int, x: ref :: $RefArrayGet($RefArraySet(A, i, x), i) == x);

 

diff --git a/Test/test0/Types1.bpl b/Test/test0/Types1.bpl
index f743be85..4c6e31ae 100644
--- a/Test/test0/Types1.bpl
+++ b/Test/test0/Types1.bpl
@@ -4,4 +4,4 @@ type V;
 function h(T) returns (int);

 function k(x:T) returns (int);

 function l(x) returns (int);  // resolve error

-function m(x:int, x) returns (bool);  // resolve error

+function m(x, x) returns (bool);  // resolve error

diff --git a/Test/test20/Answer b/Test/test20/Answer
index a4b991f7..efa5bced 100644
--- a/Test/test20/Answer
+++ b/Test/test20/Answer
@@ -87,7 +87,7 @@ type C _ _;
 

 type C2 b a = C a b;

 

-function f(C int bool) returns (int);

+function f(C int bool) : int;

 

 const x: C2 bool int;

 

@@ -108,7 +108,7 @@ type ref;
 

 type Set a = [a]bool;

 

-function union<a>(x: Set a, y: Set a) returns (Set a);

+function union<a>(x: Set a, y: Set a) : Set a;

 

 axiom (forall<a> x: Set a, y: Set a, z: a :: (x[z] || y[z]) == union(x, y)[z]);

 

@@ -133,7 +133,7 @@ implementation P()
 

 type Set a = [a]bool;

 

-function union<a>(x: Set a, y: Set a) returns (Set a);

+function union<a>(x: Set a, y: Set a) : Set a;

 

 axiom (forall<a> x: Set a, y: Set a, z: a :: x[z] || y[z] <==> union(x, y)[z]);

 

diff --git a/Test/test21/InterestingExamples4.bpl b/Test/test21/InterestingExamples4.bpl
index 371724f5..67636af1 100644
--- a/Test/test21/InterestingExamples4.bpl
+++ b/Test/test21/InterestingExamples4.bpl
@@ -14,7 +14,7 @@ axiom (forall<a,b> x:a, y:b :: sameType(x,y) == (exists z:a :: y==z));
 // b = C^n(a)

 function rel<a,b>(x:a, y:b) returns (bool);

 

-function relHelp<a,b>(x:a, y:b, int) returns (bool);

+function relHelp<a,b>(x:a, y:b, z:int) returns (bool);

 

 axiom (forall<a, b> x:a, y:b :: relHelp(x, y, 0) == sameType(x, y));

 axiom (forall<a, b> n:int, x:a, y:b ::

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;