From 9447617aefbe9706b0d74a827181976e4b9e9d26 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Thu, 17 Dec 2009 01:17:59 +0000
Subject: 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.

---
 Test/inline/Answer | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Test/inline')

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));
-- 
cgit v1.2.3