From 9c8243d39c4fc029d830dbdc4e7d6c4d7f08e3f5 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Fri, 28 Feb 2014 18:35:56 -0800
Subject: Changed all lambda-expression rewriting to be done as a
 pre-processing step before real verification. Fixed treatment of
 lambda-expression attributes.

---
 Test/test2/Answer                   |  6 +++---
 Test/test2/Lambda.bpl               |  8 ++++++++
 Test/test2/LambdaOldExpressions.bpl | 26 ++++++++++++++++++++++++--
 3 files changed, 35 insertions(+), 5 deletions(-)

(limited to 'Test/test2')

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 609cf1ed..ecec6339 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -369,7 +369,7 @@ Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
 Execution trace:
     Lambda.bpl(36,5): anon0
 
-Boogie program verifier finished with 5 verified, 2 errors
+Boogie program verifier finished with 6 verified, 2 errors
 
 -------------------- LambdaPoly.bpl --------------------
 LambdaPoly.bpl(28,5): Error BP5001: This assertion might not hold.
@@ -393,7 +393,7 @@ LambdaOldExpressions.bpl(21,3): Related location: This is the postcondition that
 Execution trace:
     LambdaOldExpressions.bpl(25,7): anon0
 
-Boogie program verifier finished with 2 verified, 1 error
+Boogie program verifier finished with 4 verified, 1 error
 
 -------------------- SelectiveChecking.bpl --------------------
 SelectiveChecking.bpl(17,3): Error BP5001: This assertion might not hold.
@@ -453,7 +453,7 @@ Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
 Execution trace:
     Lambda.bpl(36,5): anon0
 
-Boogie program verifier finished with 5 verified, 2 errors
+Boogie program verifier finished with 6 verified, 2 errors
 
 -------------------- TypeEncodingM.bpl /typeEncoding:m --------------------
 TypeEncodingM.bpl(24,3): Error BP5001: This assertion might not hold.
diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl
index 477d0f36..68c83d43 100644
--- a/Test/test2/Lambda.bpl
+++ b/Test/test2/Lambda.bpl
@@ -63,3 +63,11 @@ procedure nestedLambda()
   a := (lambda x: int :: (lambda y: int :: x+y));
 }
 
+// The following tests that the lambda in the desugaring of the
+// call command gets replaced.
+procedure P();
+  ensures (lambda y: int :: y == y)[15];
+procedure Q()
+{
+  call P();
+}
diff --git a/Test/test2/LambdaOldExpressions.bpl b/Test/test2/LambdaOldExpressions.bpl
index c26b0198..9f17245f 100644
--- a/Test/test2/LambdaOldExpressions.bpl
+++ b/Test/test2/LambdaOldExpressions.bpl
@@ -4,8 +4,8 @@ var b: bool;
 procedure p0();
   requires b;
   modifies b;
-  ensures (lambda x: bool :: old(b))[true];
-  ensures !(lambda x: bool :: b)[true];
+  ensures (lambda x: bool :: {:MyAttr "put an attr here", !b} old(b))[true];
+  ensures !(lambda x: bool :: {:AnotherAttr "yes, why not", b} {:ABC b, b, old(b)} b)[true];
 
 implementation p0()
 {
@@ -37,3 +37,25 @@ implementation p2()
     b := !b;
     assert (lambda x: bool :: old(b) != b)[true];
 }
+
+
+procedure p3();
+  requires b;
+  modifies b;
+  ensures (lambda x: int :: old(old(b)) != b)[15];
+
+implementation p3()
+{
+    b := !b;
+    assert (lambda x: int :: old(old(b)) != b)[15];
+}
+
+// Note that variables (inside and outside old expressions) mentioned
+// in attributes (even if they are not mentioned in the body of the
+// lambda) are also picked up by the auto-generated lambda functions,
+// so that the attributes can be copied to the function and axiom.
+var h: int;
+procedure TestAttributeParameters()
+  ensures (lambda x: int :: {:MyAttribute old(h), h} x < 100)[23];
+{
+}
-- 
cgit v1.2.3